The four pillars of FORSYTE are:
- Automated Program Reasoning (Kovács)
- Computer Aided Verification (Černý)
- Models Of Computation (Zuleger)
- Rigorous Systems Engineering (Weissenbacher)
The research unit is concerned with the development of both theoretical foundations and practical approaches for software and hardware verification and engineering.
Fundamental research topics include software model checking, test case generation, static analysis, protocol verification, and formal methods for distributed and concurrent systems. Industrial research is focusing on low level software, and embedded systems in the avionics and automotive sector.
We are offering courses in Formal Methods, Model Checking, Computer-Aided Verification, Abstract Interpretation, and Decision Procedures. We are always looking for enthusiastic young people who are interested in a research project or thesis in the Bachelor, Master, and PhD programs.
We regularly host talks in the RiSE seminar and VCLA talks series. This subpage summarizes the latest talks in each series - for detailed information or previous talks, please follow the links to the respective websites.
Katalin Fazekas receives Hertha Firnberg FellowshipTuesday, Jun 29, 2021
Katalin Fazekas received a Hertha Firnberg Fellowship and will (re-)join FORSYTE to perform research on Incremental SAT and SMT Reasoning for Scalable Verification. Congratulations!
Jens Pagel wins Bill McCune PhD AwardFriday, Jun 18, 2021
We congratulate Jens Pagel for receiving the 2021 Bill McCune PhD Award in Automated Reasoning! Jens graduated in 2020; his thesis on Decision procedures for separation logic: beyond symbolic heaps (supervised by Florian Zuleger) presents his substantial contributions to the theory of formal verification and automated reasoning, and to verifying heap-manipulating programs in particular.
Thanh-Hai Tran, Igor Konnov and Josef Widder win FORTE21 Best Paper AwardFriday, Jun 18, 2021
Thanh-Hai Tran, Igor Konnov and Josef Widder received the Best Paper Award at FORTE21 for their Case Study on Parametric Verification of Failure Detectors. Congratulations!
Emmanuel Pescosta nominated for EPILOG Young Alumnus AwardThursday, Jun 17, 2021
Congratulations to FORSYTE alumnus Emmanuel Pescosta, who got nominated for the Distinguished Young Alumnus award for his master’s thesis on Bounded Model Checking of Speculative Non-Interference.
ERC Consolidator Grant 2020 for Laura KovacsFriday, Dec 11, 2020
Laura Kovács has been awarded with an ERC Consolidator Grant 2020, for her project “ARTIST: Automated Reasoning with Theories and Induction for Software Technology”.
Marcel Moosbrugger wins the EPILOG Distinguished Young Alumnus awardTuesday, Dec 1, 2020
Our PhD student Marcel Moosbrugger won theEPILOG Distinguished Young Alumnus award of the TU Wien, awarding the best master thesis of master students of the Faculty of Informatics at the TU Wien in the 2020 winter semester. Congratulations!
Pavol Cerny joins FORSYTE as full professorThursday, Jul 25, 2019
We welcome Pavol Černý, who joins the FORSYTE group as a full professor of computer science in September 2019.
3 Forsyte papers accepted at CAV 2019Thursday, Apr 18, 2019
Papers co-authored by Jure Kukovec, Marijana Lazić, and Josef Widder were accepted to be presented at the 31st International Conference on Computer-Aided Verification. Title: Reachability Analysis for AWS-based NetworksAuthors: J. Backes, S. Bayless, B. Cook, C. Dodge, A. Gacek, A.J. Hu, T. Kahsai, B. Kocik, E. Kotelnikov, J. Kukovec, S. McLaughlin, J. Reed, N. Rungta, J. Sizemore, M. Stalzer, P. Srinivasan, P. Subotić, C. Varming, B. Whaley, Y. WuAbstract: Cloud services provide the ability to provision virtual networked infrastructure on demand over the internet. The rapid growth of these virtually provisioned cloud networks has increased the demand for automated reasoning tools capable of identifying misconfigurations or security vulnerabilities. This type of automation gives customers the assurance they need to deploy sensitive workloads. It can also dramatically reduce the cost and time-to-market for regulated customers looking to establish compliance certification for cloud-based applications. In this industrial case-study, we describe a new network reachability reasoning tool, called Tiros, that uses off-the-shelf automated theorem proving tools to fill this need. Tiros is the foundation of a recently introduced network security analysis feature in the Amazon Inspector service now available to millions of customers building applications in the cloud.Tiros is also used within Amazon Web Services (AWS) to automate the checking of compliance certification and adherence to security invariants for many AWS services that build on existing AWS networking features. Title: Verification of Threshold-based Distributed Algorithms by Decomposition to Decidable LogicsAuthors: Idan Berkovits, Marijana Lazić, Giuliano Lossa, Oded Padon and Sharon ShohamAbstract: Verification of fault-tolerant distributed protocols is an immensely difficult task. Often, in these protocols, thresholds on set cardinalities are used both in the process code and in its correctness proof, e.g., a process can perform an action only if it has received an acknowledgment from at least half of its peers. Verification of threshold-based protocols is extremely challenging as it involves two kinds of reasoning: first-order reasoning about the unbounded state of the protocol, together with reasoning about sets and cardinalities. In this work, we develop a new methodology for decomposing the verification task of such protocols into two decidable logics: EPR and BAPA. Our key insight is that such protocols use thresholds in a restricted way as a mean to obtain certain properties of “intersection” between sets. We define a language for expressing such properties, and present two translations: to EPR and BAPA. The EPR translation allows us to verify the protocol while assuming these properties, and the BAPA translation allows us to verify the correctness of the properties. We further develop an algorithm for automatically generating the properties needed for verifying a given protocol, facilitating a fully automated deductive verification. Using this technique we have verified several challenging benchmarks, including Byzantine one-step consensus, hybrid reliable broadcast and fast Byzantine Paxos. Title: Communication-closed asynchronous protocolsAuthors: Andrei Damian, Cezara Dragoi, Alexandru Militaru and Josef Widder.Abstract: The verification of asynchronous fault-tolerant distributedsystems is challenging due to the exponential number ofinterleavings, unbounded message buffers, and networkfailures (e.g., processes crash or message loss). We propose amethod that, for a class of protocols, reduces the verificationof asynchronous fault-tolerant protocols to the verification of around-based synchronous ones. Synchronous protocols are easierto verify due to fewer interleavings, bounded message buffersetc. We implemented our reduction method and applied it toseveral state machine replication and consensus algorithms, amongwhich are Multi-Paxos and Chandra&Toueg’s atomic broadcast. Theresulting synchronous protocols are verified using existingdeductive verification methods.Preliminary version: https://hal.inria.fr/hal-01991415v1
Deadline for Applications: Helmut Veith Stipend for Female Master´s Students in CSThursday, Nov 8, 2018
Motivated female students in the field of computer science (CS) who plan to pursue (or pursue) one of the master‘s programs in Computer Science at the Vienna University of Technology – TU Wien taught in English are invited to apply for the annually awarded Helmut Veith Stipend. The Helmut Veith Stipend is dedicated to the memory of an outstanding computer scientist who worked in the fields of logic in computer science, computer-aided verification, software engineering, and computer security. The stipend was established with support of TU Wien, the Wolfgang Pauli Institute, and generous donations of friends and colleagues of Helmut Veith. Students who are awarded the Helmut Veith Stipend, receive: EUR 6000 annually for a duration of up to two years. Waiver of all tuition fees at TU Wien. Deadline: November 30, 2018 Eligibility and how to apply: http://forsyte.at/helmut-veith-stipend/
FORSYTE's 2018 paper awardsSunday, Nov 4, 2018
FORSYTE has had a quite successful year: Adrian Rebola Pardo and his co-authors received the IJCAR best paper award for their paper Extended Resolution Simulates DRAT, Mitra Tabaei Befrouei and her co-authors received an OOPSLA 2018 Distinguished Paper award for their paper Randomized Testing of Distributed Systems with Probabilistic Guarantees, and Thomas Pani received the FMCAD Best Student Contribution Award for his contribution Rely-Guarantee Reasoning for Automated Bound Analysis of Concurrent, Shared-Memory Program (the second year in a row). Congratulations!
OOPSLA Distinguished Paper AwardThursday, Oct 18, 2018
Mitra Tabaei Befrouei and her co-authors from MPI-SWS Burcu Kulahcioglu Ozkan, Rupak Majumdar, and Filip Niksic, received an OOPSLA’18 Distinguished Paper Award for their contribution “Randomized Testing of Distributed Systems with Probabilistic Guarantees” (Open Access article). Congratulations!
Zvonimir Rakamiric visiting FORSYTEWednesday, Oct 3, 2018
Prof. Zvonimir Rakamiric from the School of Computing at the University of Utah is spending his sabbatical with the FORSYTE group at TU Wien. He is generously sponsored by the Wolfgang Pauli Institute and a Pauli Fellow.
Helmut Veith Stipend Award CeremonyWednesday, Apr 4, 2018
The Vice Rector for Academic Affairs of TU Wien, Kurt Matyas, will award the scholarship recipient of the Helmut Veith Stipend at the award ceremony on Friday, April 06, 2018 in the Kontaktraum, starting at 17:05. Helmut Veith Stipend The annually awarded Helmut Veith Stipend for female master students is dedicated to the memory of an outstanding computer scientist who worked in the fields of logic in computer science, computer-aided verification, software engineering, and computer security. Helmut Veith, who tragically passed away in March 2016, was a strong advocate and mentor for women in computer science. His great polymathic mind interested in application of formal and logical methods to problems in software technology and engineering, resonates in his legacy. The Helmut Veith Stipend was established with generous support of TU Wien, Wolfgang Pauli Institute and with contributions by family and friends of the late Helmut Veith. Application for Helmut Veith Stipend 2018/2019 is open. Download the flyer here.
FORSYTE organizes CAV 2018Wednesday, Jan 10, 2018
The FORSYTE group is co-organizing the 30th International Conference on Computer Aided Verification (CAV), which will take place in Oxford from July 14-17, 2018, as part of the Federated Logic Conference (FLoC). CAV is the leading conference on theory and practice of computer-aided formal verification for hardware and software systems. The paper submission deadline is January 31, 2018 (see our Call for Papers). Please consider submitting your work to CAV, and join us in July in Oxford!
FMSD Special Issue in Memoriam Helmut VeithThursday, Nov 16, 2017
In memory of Helmut Veith, the founder of the FORSYTE research group, the current issue of the Journal on Formal Methods in System Design is a Special Issue in Memoriam Helmut Veith.Helmut unexpectedly passed away in March 2016; he was a brilliant researcher, inspiring collaborator, passionate mentor, generous friend, and valued member of the formal methods community. Helmut was not only known for his numerous and influential contributions in the field of automated verification (most prominently his work on Counterexample-Guided Abstraction Refinement), but also for his untiring and passionate efforts for the logic community. He is sorely missed. Link to the Special Issue (Volume 51, Issue 2, November 2017).
Helmut Veith Stipend 2017: Deadline Extension (November 30)Thursday, Sep 7, 2017
The application deadline for the Helmut Veith Stipend 2017 has been extended to November 30.The stipend is dedicated to the memory of an outstanding computer scientist who worked in the fields of logic in computer science, computer-aided verification, software engineering, and computer security. We encourage all female master’s students attending (or planning to attend) one of the master’s courses in Computer Science at TU Wien taught in English to apply. Details are available on http://forsyte.at/helmut-veith-stipend.
Helmut Veith Stipend 2017Tuesday, Jul 11, 2017
Outstanding female students in the field of computer science who pursue (or plan to pursue) one of the master‘s programs in Computer Science at TU Wien taught in English are invited to apply for the Helmut Veith Stipend The stipend is dedicated to the memory of an outstanding computer scientist who worked in the fields of logic in computer science, computer-aided verification, software engineering, and computer security. Students who are awarded the Helmut Veith Stipend, which is co-funded by TU Wien, receive EUR 6000 annually for a duration of up to two years. In addition, all tuition fees are waived. Recipients of funding must demonstrate good progress during their studies and will have to reside in Austria during term time for the duration of their studies. The extended application deadline for 2017 is November 30. Find out more.
Summer School on Logic, Artificial Intelligence and VerificationFriday, May 5, 2017
The doctoral college Logical Methods in Computer Science (LogiCS) and the Austrian Society for Rigorous Systems Engineering (RiSE) will host a summer school on Logic, Artificial Intelligence and Verification at TU Wien, Vienna, Austria from July 3 to July 5.
Helmut Veith StipendTuesday, Mar 7, 2017
The first recipient of the Helmut Veith Stipend for excellent female master’s students in computer science will be presented on March 14 at the following event: "More female students in computer science. Who cares?" Panel discussion with renowned scientists about diversity in STEM Studies March 14, 5:30pm, TU Wien The Helmut Veith Stipend is dedicated to the memory of an outstanding computer scientist who worked in the fields of logic in computer science, computer-aided verification, software engineering, and computer security. The stipend is awarded annually to excellent female students who pursue a master’s program taught in English at TU Wien (see eligibility details). The application deadline for this year’s Helmut Veith Stipend is August 20, 2017.
Congratulations, Dr. Mitra Tabaei BefroueiSaturday, Jan 14, 2017
Mitra Tabaei Befrouei successfully defended her doctoral thesis on "Effective Error Explanation Techniques for Concurrent Software" on December 6, 2016. The FORSYTE group congratulates the newly-minted Doctor!
WAIT 2016 in ViennaFriday, Nov 11, 2016
The third WAIT workshop on induction is held between 17-18 November at the TU Wien. Details are available on the workshop page.
Two papers at POPL’17Tuesday, Oct 4, 2016
Two papers co-authored by researchers from our group have been accepted for POPL’17: “Coming to Terms with Quantified Reasoning” by Simon Robillard, Andrei Voronkov, and Laura Kovacs; and “A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms” by Igor Konnov, Marijana Lazic, Helmut Veith, and Josef Widder
Helmut Veith StipendMonday, Oct 3, 2016
Outstanding female students in the field of computer science who pursue (or plan to pursue) one of the master‘s programs in Computer Science at TU Wien taught in English are invited to apply for the Helmut Veith Stipend The stipend is dedicated to the memory of an outstanding computer scientist who worked in the fields of logic in computer science, computer-aided verification, software engineering, and computer security. Students who are awarded the Helmut Veith Stipend, which is co-funded by TU Wien, receive EUR 6000 annually for a duration of up to two years. In addition, all tuition fees are waived. Recipients of funding must demonstrate good progress during their studies and will have to reside in Austria during term time for the duration of their studies. The application deadline is November 30, 2016. Find out more here or download the PDF flyer. Photo credits: Nadja Meister
LogicLounge in memoriam Helmut VeithFriday, Jul 15, 2016
Will robots take away your job? In memory of Helmut Veith, this year’s Conference on Computer Aided Verification (CAV), which takes place in Toronto, will feature a LogicLounge on the effect of automation and artificial intelligence on our jobs.The LogicLounge discussion series was initiated during the Vienna Summer of Logic 2014 and aims to provide a public forum for the discussion of computer science topics. In the upcoming installment on July 22, 2016, Artificial Intelligence professor Moshe Y. Vardi (Rice University, USA) will discuss with journalist Dan Falk if, when, and how robots will take over human jobs. Or have they already? Details about this event can be found on the VCLA LogicLounge website.
Marijana Lazić wins ZONTA mobility stipendThursday, Jul 7, 2016
Marijana Lazić won the “ZONTA CLUB WIEN I – TU-Mobilitätsstipendium” for her research in the intersection of computer-aided verification and distributed computing theory.The stipend will support her in attending international conferences in the concerned research areas. Supported by ZONTA, she is already on a trip to the US and Canada to attend this year’s LICS and CAV conferences. Later this year, she will visit the University of California, Berkeley for several months. We are very happy for Marijana!
Questions answered by Leslie LamportFriday, May 27, 2016
Leslie Lamport is going to answer questions about a Mathematical View of Computer Systems in Informatikhörsaal on Tuesday at 6pm. Check the announcement at the VCLA website and do not forget to watch the lecture beforehand.
Laura Kovács joins FORSYTE as full professorSaturday, Apr 9, 2016
We welcome Laura Kovács, who joined the FORSYTE group as a full professor of computer science in April 2016.Laura also holds a part-time associate professorship at the Chalmers University of Technology, Sweden. Her research deals with the design and development of new theories, technologies, and tools for program analysis, with a particular focus on automated assertion generation, symbolic summation, computer algebra, and automated theorem proving. She is the co-developer of the Vampire theorem prover. In 2014, she received the prestigious Wallenberg Academy Fellowship and an ERC Starting Grant. She holds an MSc from the Western University of Timisoara, Romania, and a PhD degree from the Research Institute for Symbolic Computation of the Johannes Kepler University, Linz, Austria. After her PhD studies, from 2007 to 2010 she was a postdoctoral researcher in the Models and Theory of Computation research group of Prof. Dr. Thomas A. Henzinger at the Swiss Federal Institute of Technology Lausanne (EPFL), and at the Programming Methodology research group of Prof. Dr. Peter Müller at the Swiss Federal Institute of Technology Zürich (ETH). From 2010 to 2013, she was a FWF Hertha Firnberg Research Fellow and an assistant professor at the Institute of Computer Languages of the TU Wien. Since 2012, she holds a habilitation degree in computer science from the TU Wien.
Spring School on Logic and VerificationTuesday, Mar 22, 2016
The Spring School on Logic and Verification (LOVE 2016) is going to take place in Vienna from April 15 to 17 – early registration ends on March 25. Details are available on our webpage.
Helmut Veith 1971-2016Monday, Mar 14, 2016
It is with the deepest sadness that we announce Helmut Veith’s passing on March 12, 2016. Helmut was a brilliant researcher, an inspiring collaborator, a stimulating teacher, a generous friend, and a wonderful father and husband. He leaves a void that will be impossible to fill. Our thoughts are with his family and friends.Funeral speech by Georg Gottlob Obituary by Thomas Eiter: German and English Obituary by Richard Zach (English) Obituary by Oliver Lehmann (English) Obituary by Florian Aigner (German) Obituary by the students of the Doctoral College Logical Methods in Computer Science (English) Commemorative booklet (Russian-English) Personal statement by Dana Scott about Helmut (video recording, starting at 48:40) If you have photos of Helmut (or him together with his friends) which you would like to share with others, please send them to Mihaela Rozman at mihaela.rozman(@)tuwien.ac.at. In memory of Helmut, we have established a stipend to support outstanding female master’s students. We are asking for contributions. Contributions to the Helmut Veith Stipend can be made to “Zentrum für Informatikforschung”, IBAN: AT36 1200 0515 8258 2701, BIC: BKAUATWW, reference: “Helmut Veith Stipend” or by credit card via PayPal
CFP: Formal Reasoning in Distributed Algorithms (FRIDA’16)Friday, Feb 26, 2016
Josef Widder and Igor Konnov are co-organizing the third workshop on Formal Reasoning in Distributed Algorithms. Check the workshop page.
The paper following the invited talk by Helmut Veith at PSI’15Friday, Feb 12, 2016
If you wanted to know anything about model checking of fault-tolerant distributed algorithms, then check our follow-up paper after the invited talk by Helmut Veith at PSI’15.
Profil article on women in logicSaturday, Dec 26, 2015
A recent article in the Austrian weekly Profil about female logicians in Austria is featuring Agata Ciabattoni, Martina Seidl, Laura Kovacs, Magdalena Ortiz, Marijana Lazic, Shqiponja Ahmetaj, and Neha Lodha. All women are affiliated with the Doctoral College Logical Methods in Computer Science.
Congratulations, Dr. Annu GmeinerWednesday, Nov 18, 2015
Annu Gmeiner defended her PhD thesis on parameterized verification of fault-tolerant distributed algorithms. Congratulations!
Panel discussion on research funding in AustriaWednesday, Nov 18, 2015
Helmut Veith was a panelist in a public discussion on research funding in Austria. Link to event poster Link to Der Standard newspaper report
The book on "Decidability of Parameterized Verification" is publishedWednesday, Sep 30, 2015
The book by Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder on Decidability of Parameterized Verification has just been published.
WWTF ICT project awarded to Igor KonnovThursday, Sep 17, 2015
Igor Konnov (PI), together with Josef Widder (co-PI) and Helmut Veith (core team), are awarded an ICT research project APALACHE “Abstraction-based Parameterized TLA Checker” by the Vienna Science and Technology Fund WWTF.
Austrian Computer Science Day 2015Tuesday, Sep 1, 2015
The Austrian Computer Science Day 2015, which takes place on October 15, features a range of talks by leading Austrian computer scientists, including topics such as computer games, augmented reality, aware systems, semantic web, business processes, and reliable systems. Register for free by October 7, 2015! This year’s speakers are: Alois Ferscha (JKU Linz) Tom Henzinger (IST Austria) Magdalena Ortiz (TU Wien) Radu Prodan (Innsbruck) Stefanie Rinderle-Ma (Uni Wien) Dieter Schmalstieg (TU Graz) Emo Welzl (ETH Zuerich) Britta Schinzel (University of Freiburg) will talk about Ada Lovelace at the Kick-Off Event on October 14 (joint event with the European Computer Science Summit).
Helmut Veith receives CAV AwardSaturday, Aug 1, 2015
The 2015 CAV Award is given to Edmund Clarke, Orna Grumberg, Ron Hardin, Zvi Harel, Somesh Jha, Robert Kurshan, Yuan Lu, and Helmut Veith for the development and implementation of the localization-reduction technique and the formulation of counterexample-guided abstraction refinement (CEGAR). CAV 2015 website
Congratulations to Privatdozent Josef WidderThursday, Jul 2, 2015
Josef Widder has received his habilitation in computer science from TU Wien. He is now Privatdozent.
FRIDA’15Friday, Jun 5, 2015
We had great talks at FRIDA’15 workshop in Grenoble. The slides of some of the talks are available online.
FRIDA’15 ProgramSunday, May 10, 2015
Check the program of the 2nd workshop on Formal Reasoning in Distributed Algorithms at FORTE. We have a nice program this year.
iDQ solver onlineWednesday, Jul 2, 2014
iDQ v1.0 is now available online: http://forsyte.at/software/idq/
FRIDA Progam OnlineWednesday, Jun 11, 2014
We have a great program for our workshop on formal reasoning in distributed algorithms. Join us at the workshop!
iPrA Workshop on InterpolationTuesday, Jun 10, 2014
Laura Kovács and Georg Weissenbacher are the organizers of the second workshop on Craig interpolation and its applications.After a very successful first edition of the workshop in St. Petersburg in 2013 (co-located with the CAV conference, which was also organized by the Forsyte group), the second workshop has an even stronger focus on bringing researchers from different communities together: the workshop features three distinguished invited speakers from the fields of complexity theory, description logics, and verification, and 14 talks on theoretical aspects of interpolation as well as applications in decision procedures, game theory, synthesis, verification, and description logics.
SAT/SMT Summer School 2014Tuesday, Jun 10, 2014
The Forsyte group co-organises this year’s edition of the SAT/SMT Summer School.We have invited 12 internationally renowned experts in the field of automated decision procedures to present the foundations as well as applications of SAT/SMT solvers. We received 125 applications, of which we invited more than 80 international participants from Asia, the Americas, and Europe.
Imagine Josef WidderTuesday, Jun 3, 2014
Josef Widder is invited to talk tomorrow at Imagine 14 about how research funding started his IT career.
Funded Doctoral Positions in Computer ScienceWednesday, May 7, 2014
TU Wien, TU Graz, and JKU Linz are seeking exceptionally talented and motivated students for their joint doctoral program LogiCS.The LogiCS doctoral college focuses on interdisciplinary research topics covering (i) computational logic, and applications of logic to (ii) databases and artificial intelligence as well as to (iii) computer-aided veriﬁcation. The Program LogiCS is a doctoral college focusing on logic and its applications in computer science. Successful applicants will work with and be supervised by leading researchers in the fields of computational logic, databases and knowledge representation, and computer-aided verification. Faculty Members M. Baaz A. Biere R. Bloem A. Ciabattoni U. Egly T. Eiter C. Fermuller R. Grosu A. Leitsch M. Ortiz R. Pichler S. Szeider H. Tompits H. Veith G. Weissenbacher Details are provided on http://logic-cs.at/phd/faculty/ Positions and Funding We are looking for 1-2 doctoral students per faculty member, where 30% of the positions are reserved for highly qualiﬁed female candidates. The doctoral positions are funded for a period of 3 years according to the funding scheme of the Austrian Science Fund. The funding can be extended for one additional year contingent on a placement at one of our international partner institutions. How to Apply Detailed information about the application process is available on the LogiCS web-page http://logic-cs.at/phd/ The applicants are expected to have completed an excellent diploma or master’s degree in computer science, mathematics, or a related ﬁeld. Candidates with comparable achievements will be considered on a case-by-case basis. Applications by the candidates need to be submitted electronically. Highest Quality of Life The Austrian cities Vienna, Graz, and Linz, located close to the Alps and surrounded by beautiful nature, provide an exceptionally high quality of life, with a vibrant cultural scene, numerous cultural events, world-famous historical sites, a large international community, a varied cuisine and famous coﬀee houses.
CAV Workshop FRIDATuesday, Apr 15, 2014
Igor Konnov and Josef Widder are organizing the CAV Workshop FRIDA.
Master’s thesis topic on automated SAT-based cryptanalysis availableTuesday, Apr 15, 2014
The topic of this thesis is to improve an automated SAT-based cryptanalsis approach. There is the opportunity to work on this thesis during an internship at a large financial institution. If you are interested please contact Andreas Holzer.
New CBMC-GC version onlineFriday, Mar 28, 2014
The new version 0.9.3 of CBMC-GC is now available online: http://forsyte.at/software/cbmc-gc/
15 FWF funded PhD positions in doctoral college "Logical Methods in Computer Science"Tuesday, Feb 25, 2014
FWF has approved a doctoral college for Logical Methods in Computer Science. Details are available on the LogiCS website.
Janos Makowsky visiting in spring 2014Saturday, Feb 22, 2014
Janos Makowsky from Technon will be a visiting professor of the European Master Program in Computational Logic. He will teach a course on Graph Polynomials.
Facebook group for Austrian computer scientistsSunday, Jul 21, 2013
There is a new facebook group for communication among Austrian computer scientists: https://www.facebook.com/groups/AustrianComputerScience/ For those who are skeptical about facebook, we created a read-only mirror (beta version): http://forsyte.at/acs/
Johannes Kinder joins Royal HollowaySaturday, Jul 20, 2013
After a postdoc with George Candea, FORSYTE alumnus Johannes Kinder will start a lecturer position at Royal Holloway in September 2013! Congratulations! http://people.epfl.ch/johannes.kinder?lang=en&cvlang=
Michael Tautschnig joins Queen Mary, University of LondonSunday, Jun 9, 2013
After a postdoc in Daniel Kroening’s group, FORSYTE alumnus Michael Tautschnig is joining Queen Mary as a Lecturer. Congratulations! http://www.eecs.qmul.ac.uk/people/view/33534/dr-michael-tautschnig
Doron Peled visiting May 2013Thursday, May 9, 2013
Doron Peled is visiting our group for a month in May 2013.
2nd Austrian Computer Science DaySunday, Apr 21, 2013
We are co-organizing the Austrian Computer Science Day 2013 at IST Austria. http://ist.ac.at/austrian-computer-science-day-2013/
Dagstuhl Workshop "Formal Verification of Distributed Algorithms" coorganized by Josef WidderThursday, Mar 21, 2013
Josef Widder is organizing an interdisciplinary Dagstuhl workshop http://www.dagstuhl.de/en/program/calendar/semhp/?semnr=13141 This is part of a continuing effort in the RiSE project http://rise.or.at to establish closer links between distributed algorithms and computer-aided verification.
CAV 2013 in St. Petersburg!Wednesday, Oct 10, 2012
Our group is co-organizing CAV 2013, the leading conference in computer-aided verification. The conference will take place July 13-19, 2013, during the famous White Nights in beautiful St. Petersburg.
Florian Zuleger in the Austrian Newspaper "Der Standard"Wednesday, Oct 3, 2012
Florian gave an interview about his research on bound computation to the Austrian daily newspaper “Der Standard”.
Joint Workshop between CMACS and RiSE in Washington, DCThursday, Sep 27, 2012
Adjoint to the Austrian science talks in Washington, DC, our group participated in a joint workshop between CMACS and RiSE.
Ten funded PhD and PostDoc positionsMonday, Jul 9, 2012
The Formal Methods in Systems Engineering Group at Vienna University of Technology offers 10 PhD/PostDoc positions. We are looking for new colleagues in the areas of Formal Methods, Software Model Checking, Abstract Interpretation, Static Analysis, Automata Theory, … If you are mathematically inclined and/or a versatile programmer willing to combine theory and practice, one of these research projects might offer the job of your dreams.
Florian Zuleger winning WWTF grantTuesday, Jun 26, 2012
Florian Zuleger was awarded a grant by WWTF for his research project “Automated Program Analysis for Bounds on Resource Consumption”. Florian’s project will develop new methods to extract bounds for loops, memory and bandwidth from imperative programs.http://www.wwtf.at/programmes/ict/#c1934h
Welcome Georg WeissenbacherTuesday, Jun 26, 2012
Georg Weissenbacher, leader of a WWTF funded Vienna Research Group, will start his work in our group on July 2. His project “Heisenbugs: From Detection to Explanation” is applying formal methods to identify hard-to-detect errors in computer systems. See a newspaper article on his work in “Der Standard”.
Uni-Finanzierung als Absurdes Theater (Der Standard)Wednesday, Mar 28, 2012
An sieben Universitäten werden in Österreich Informatik-Studien angeboten, aber mehr als 50 Prozent der Studierenden wählen die TU Wien – über 1000 Studienanfänger jährlich. Der gute Ruf der TU Wien wird zum Fluch für das Studium, denn auf 52 habilitierte Professoren kommen fast 7000 Studierende; ein solches Verhältnis wäre bei anderen international führenden Universitäten undenkbar. Alle wissen, dass Mangelwirtschaft an Universitäten dem Wissenschafts- und Wirtschaftsstandort schadet, die Innovationskraft unserer Gesellschaft untergräbt und den wissenschaftlichen Nachwuchs ins Ausland treibt. DerStandard
Doctoral College “Adaptive Distributed Systems”Wednesday, Mar 21, 2012
The Doctoral College “Adaptive Distributed Systems” intends to work on the challenging questions of today’s distributed computer systems by bringing together experts from various fields of computer science, mathematics and statistics, thus fostering a multidisciplinary approach. Call for applications 2012/2013: Continuous filling has started and new applications are welcome Ultimate closing: March 15th, 2013 Start of program: Winter semester 2012 (phase-in) Please visit the website for more information.
Upcoming Course: Ana SokolovaFriday, Feb 24, 2012
Ana Sokolova from the University of Salzburg will be visiting as a guest lecturer for the course “Coalgebra in Computer Science”. Thu 14:00 – 16:00 08.03.2012 Seminarraum GödelThu 14:00 – 16:00 15.03.2012 Seminarraum GödelThu 14:00 – 16:00 22.03.2012 Seminarraum GödelThu 14:00 – 16:00 19.04.2012 Seminarraum GödelThu 14:00 – 16:00 26.04.2012 Seminarraum GödelThu 14:00 – 16:00 03.05.2012 Seminarraum von NeumannThu 14:00 – 16:00 24.05.2012 Seminarraum GödelThu 14:00 – 16:00 31.05.2012 Seminarraum GödelThu 14:00 – 16:00 14.06.2012 Seminarraum GödelThu 14:00 – 16:00 21.06.2012 Seminarraum GödelThu 14:00 – 16:00 28.06.2012 Seminarraum Gödel Registration and further details in TISS. Goals: The goal is to get acquainted with the theory of coalgebra and its use in computer science. Also, along the way, the students will get to know some category theory notions that are needed for basic constructions and results in coalgebra. The course is meant for computer science students (possibly also some mathematics students) interested in computer science theory. If you are a student interested in formal methods, concurrency theory, and/or automata, and/or you always wondered what is category theory good for, then this may be the right course for you. Content: The theory of coalgebra is a relatively recent (20 years old) unifying theory at the abstract end of formal methods. It is a (one could say “the”) theory of dynamic systems, of states and observations. Coalgebras allow for a uniform treatment of many different types of automata (e.g. deterministic, nondeterministic, probabilistic, and weighted), their behavior, and their corresponding modal logics. These topics will be covered within the course. How students are evaluated:The evaluation will depend on presented papers and the examination at the end of term. ECTS-Breakdown (3 ECTS): ————————–30 hours: lectures23 hours: exercises23 hours: preparation for examination2 hours: examination————————–75 hours: total————————–
Upcoming Course: Johannes FürnkranzThursday, Feb 23, 2012
Johannes Fürnkranz from TU Darmstadt will be visiting as a guest lecturer for the course: VO Inductive Rule Learning Mon 08:30 – 13:00 12.03.2012 seminar room Gödel Tue 08:30 – 13:00 13.03.2012 seminar room Gödel Mon 12:30 – 17:00 19.03.2012 seminar room Gödel Mon 08:30 – 13:00 26.03.2012 seminar roomGödel Tue 08:30 – 13:00 27.03.2012 seminar room Gödel Registration and further details in TISS. Aim of the course: The goal of this course to familiarize the student with fundamental concepts of machine learning in general and inductive rule learning in particular. It will focus both on a predictive setting, where the goal is to learn a set of rules that collectively make a prediction, and a descriptive setting, where the goal is to learn a set of rules that collectively explain the data. The learning techniques will be first illustrated for concept learning tasks in propositional logic, but later also extended to first-order logic as well as to structured prediction tasks. There are no prerequisites except for basic knowledge about algorithms. The course is thus not only suited for computer science students but for all students that have a strong interest in machine learning in data analysis. Content: Rules – the clearest, most explored and best understood form of knowledge representation – are particularly important for data mining, because they offer the best tradeoff between human and machine understandability. This course will present algorithms for automated rule learning and discovery as investigated in classical machine learning and modern data mining. We will start with algorithms for learning single rules in propositional logic, move on to learning rule sets with the covering or separate-and-conquer algorithm, inductive logic programming algorithms for learning rules in first-order logic, and discuss approaches that allow to make predictions in structured output spaces. Elementary data mining algorithms such as association rule discovery will also be covered, as well as essential concepts of machine learning and data mining. It is thus suitable as a first introduction into these research areas. Most of the course will follow the book “Foundations of Rule Learning” that will appear in Springer-Verlag in early 2012. http://www.amazon.de/Rule-Learning-Essentials-Relational-Technologies/dp/3540751963
Opening of Vienna Center for Logic and Algorithms (VCLA) on Jan 25Friday, Jan 13, 2012
The Vienna Center for Logic and Algorithms is an initiative of the Faculty of Informatics and funded by a three-year competitive grant of Vienna University of Technology. Embedded into the primary research area Computational Intelligence and the funding priority Computational Logic of the Faculty, the center is promoting international scientific collaboration in logic and algorithms. We will celebrate the opening of VCLA with a Symposium on January 25. See the VCLA website for details.
TU Vienna Honorary Doctorate to Ed ClarkeFriday, Jan 13, 2012
We are glad to announce that TU Vienna will award an honorary doctorate to Ed Clarke. Edmund M. Clarke is among the leading computer scientists of our times. As a professor at Harvard, and, since 1982, at Carnegie Mellon University, he and his group have not only laid the theoretical and logical foundations of model checking (ACM Turing Award, 2007), but also pioneered model checking as a powerful tool for industrial hardware and software engineering. On January 26, 2012, as part of the festive opening of the Vienna Center for Logic and Algorithms, Prof. Clarke will be awarded an honorary doctorate from TU Vienna in recognition of his contributions to Computer Science. Below: Ed Clarke at the Opening Press Conference of the RiSE Network in March 2011
Happy New Year 2012!Friday, Jan 6, 2012
The FORSYTE team is wishing our friends, colleagues and students a Happy New Year!
Winter School on VerificationThursday, Dec 8, 2011
The Austrian Society for Rigorous Systems Engineering (ARiSE) and the Vienna Center for Logic and Algorithms (VCLA) are organizing a joint winter school on verification at Vienna University of Technology from 6-10 February 2012. Apart from ARiSE/VCLA students, the school will be open to outside students. Details are available from the VCLA website.
Joint PUMA/ARiSE Workshop in TraunkirchenMonday, Oct 10, 2011
From October 3–7 2011 PUMA and ARiSE held a joint workshop in Traunkirchen. Further information is available from the workshop’s website. Photos by Damien Zufferey (full gallery):
Helmut Veith is a founding member of the Austrian Society for Rigorous Systems EngineeringFriday, May 28, 2010
The Austrian Society for Rigorous Systems Engineering (ARiSE) was founded in 2010 to further the research in formal methods for the design of correct computer systems. It brings together top researchers in formal methods in Austria in order to foster collaboration and a common research platform.
CfP: Workshop on Exploiting Concurrency Efficiently and Correctly (EC^2 2010)Tuesday, Mar 30, 2010
The annual Workshop on Exploiting Concurrency Efficiently and Correctly (EC2) is a forum that brings together researchers working on formal methods for concurrency, and those working on advanced parallel applications. Its goal is to stimulate incubation of ideas leading to future concurrent system design an verification tools that are essential in the multi-core era.