Research
The four pillars of FORSYTE are:
- Automated Program Reasoning (Kovács)
- Theory and Applications of Satisfiability (Fazekas)
- 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.
more...
Teaching
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.
more...
Talks
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.
more...
Recent news
New doctoral program on Automated Reasoning
Thursday, Dec 5, 2024We are happy to announce a new FWF doc.funds doctoral program on Automated Reasoning, with funding for 13 doctoral students who will work on exciting projects at the intersection of security and artificial intelligence with Automated Reasoning at the core. The doctoral program is designed to educate the next generation of experts on Automated Reasoning. It targets foundational questions such as rigorously defining the notion of safety and security across domains and applications, the development of automated techniques and analyses to ensure safety and security of electronic systems, and explores synergies between the fields of security and artificial intelligence. The doctoral students will be supervised by the FORSYTE professors Katalin Fazekas, Laura Kovács, and Georg Weissenbacher together with Ezio Bartocci, Maria Christakis, Thomas Gärtner, and Mattei Maffei. See also the announcements of TU Wien and FWF (in German).
Ivana Bocevska wins Siemens Award of Excellence
Wednesday, Dec 4, 2024The faculty has awarded a Siemens Excellence Award to our master student Ivana Bocevska, who is being supervised by Laura Kovács during her master studies. Congratulations!
FORSYTE team secures third place in CSAW Student Cybersecurity Competition
Wednesday, Nov 20, 2024Lea Salome Brugger, a former master’s student at TU Wien and now a PhD student at ETH Zürich, won 3rd place at the CSAW Applied Research Competition in cybersecurity. She presented the paper “CheckMate: Automated Game-Theoretic Security Reasoning,” co-authored with Laura Kovács, Anja Petković Komel, Sophie Rain, and Michael Rawson. Read the full article here.
Robin Coutelier awarded with the Paul Gauchet Fondation Prize
Friday, Nov 15, 2024Robin Coutelier was awarded with the Paul Gochet Prize by the University of Liège for his master thesis on "Chronological vs. Non-Chronological Backtracking in SMT". The funding aims at supporting his collaboration with researchers at his former University. The Fondation Paul Gochet was funded to support research in the field of Logic around the University of Liège.
Abenteuer Informatik featured in Der Standard
Wednesday, Oct 23, 2024Abenteuer Informatik, initiated by FORSYTE members in 2022, was featured in the online edition of Der Standard. Read the article here.
Two successful PhD thesis defenses at FORSYTE
Monday, Jun 24, 2024Petra Hozzova successfully defended her PhD thesis "Inductive Reasoning in Superposition" and Marcel Moosbrugger also successfully defended his PhD thesis "Automated Analysis of Probabilistic Loops". Congratulations!
Pamina Georgiou successfully defended her PhD thesis
Monday, Mar 25, 2024Pamina Georgiou has successfully defended her PhD thesis titled "Towards Automating Induction for Software Verification Guiding Inductive Reasoning in Superposition-based Theorem Proving". Congratulations!
Katalin Fazekas receives Hertha Firnberg Fellowship
Tuesday, Jun 29, 2021Katalin 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 Award
Friday, Jun 18, 2021We 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 Award
Friday, Jun 18, 2021Thanh-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 Award
Thursday, Jun 17, 2021Congratulations 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 Kovacs
Friday, Dec 11, 2020Laura 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 award
Tuesday, Dec 1, 2020Our 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 professor
Thursday, Jul 25, 2019We welcome Pavol Černý, who joins the FORSYTE group as a full professor of computer science in September 2019.
3 Forsyte papers accepted at CAV 2019
Thursday, Apr 18, 2019Papers 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 CS
Thursday, Nov 8, 2018Motivated 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 awards
Sunday, Nov 4, 2018FORSYTE 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 Award
Thursday, Oct 18, 2018Mitra 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 FORSYTE
Wednesday, Oct 3, 2018Prof. 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 Ceremony
Wednesday, Apr 4, 2018The 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 2018
Wednesday, Jan 10, 2018The 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 Veith
Thursday, Nov 16, 2017In 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).
FRIDA’17 at DISC
Monday, Oct 16, 2017We have a great program at FRIDA’17 that takes place in Vienna
Helmut Veith Stipend 2017: Deadline Extension (November 30)
Thursday, Sep 7, 2017The 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 2017
Tuesday, Jul 11, 2017Outstanding 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 Verification
Friday, May 5, 2017The 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 Stipend
Tuesday, Mar 7, 2017The 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 Befrouei
Saturday, Jan 14, 2017Mitra 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 Vienna
Friday, Nov 11, 2016The 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’17
Tuesday, Oct 4, 2016Two 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 Stipend
Monday, Oct 3, 2016Outstanding 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 Veith
Friday, Jul 15, 2016Will 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 stipend
Thursday, Jul 7, 2016Marijana 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 Lamport
Friday, May 27, 2016Leslie 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.
FRIDA 2016 in Marocco
Monday, May 23, 2016We had nice talks at the workshop on Formal Reasoning in Distributed Algorithms (FRIDA) this year. Look at the workshop web page.
Laura Kovács joins FORSYTE as full professor
Saturday, Apr 9, 2016We 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 Verification
Tuesday, Mar 22, 2016The 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-2016
Monday, Mar 14, 2016It 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, 2016Josef 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’15
Friday, Feb 12, 2016If 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 logic
Saturday, Dec 26, 2015A 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 Gmeiner
Wednesday, Nov 18, 2015Annu Gmeiner defended her PhD thesis on parameterized verification of fault-tolerant distributed algorithms. Congratulations!
Panel discussion on research funding in Austria
Wednesday, Nov 18, 2015Helmut 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 published
Wednesday, Sep 30, 2015The 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 Konnov
Thursday, Sep 17, 2015Igor 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 2015
Tuesday, Sep 1, 2015The 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 Award
Saturday, Aug 1, 2015The 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 Widder
Thursday, Jul 2, 2015Josef Widder has received his habilitation in computer science from TU Wien. He is now Privatdozent.
FRIDA’15
Friday, Jun 5, 2015We had great talks at FRIDA’15 workshop in Grenoble. The slides of some of the talks are available online.
FRIDA’15 Program
Sunday, May 10, 2015Check the program of the 2nd workshop on Formal Reasoning in Distributed Algorithms at FORTE. We have a nice program this year.
Josef Widder is awarded a FWF standalone project
Friday, Mar 20, 2015Josef Widder is awarded a FWF standalone project “PRAVDA” on Parameterized Verification of Fault-tolerant Distributed Algorithms
iDQ solver online
Wednesday, Jul 2, 2014iDQ v1.0 is now available online: http://forsyte.at/software/idq/
FRIDA Progam Online
Wednesday, Jun 11, 2014We have a great program for our workshop on formal reasoning in distributed algorithms. Join us at the workshop!
iPrA Workshop on Interpolation
Tuesday, Jun 10, 2014Laura 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 2014
Tuesday, Jun 10, 2014The 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 Widder
Tuesday, Jun 3, 2014Josef Widder is invited to talk tomorrow at Imagine 14 about how research funding started his IT career.
Funded Doctoral Positions in Computer Science
Wednesday, May 7, 2014TU 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 verification. 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 qualified 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 field. 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 coffee houses.
CAV Workshop FRIDA
Tuesday, Apr 15, 2014Igor Konnov and Josef Widder are organizing the CAV Workshop FRIDA.
Master’s thesis topic on automated SAT-based cryptanalysis available
Tuesday, Apr 15, 2014The 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 online
Friday, Mar 28, 2014The 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, 2014FWF has approved a doctoral college for Logical Methods in Computer Science. Details are available on the LogiCS website.
Janos Makowsky visiting in spring 2014
Saturday, Feb 22, 2014Janos Makowsky from Technon will be a visiting professor of the European Master Program in Computational Logic. He will teach a course on Graph Polynomials.
Vienna Summer of Logic 2014
Friday, Feb 21, 2014Our group is coorganizing the Vienna Summer of Logic, the largest conference in the history of logic. http://vsl2014.at
Facebook group for Austrian computer scientists
Sunday, Jul 21, 2013There 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 Holloway
Saturday, Jul 20, 2013After 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=
Aaron Bradley visiting June 2013
Sunday, Jun 23, 2013Aaron Bradley is visiting our group for June 2013, and teaching a course on IC3.
Michael Tautschnig joins Queen Mary, University of London
Sunday, Jun 9, 2013After 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 2013
Thursday, May 9, 2013Doron Peled is visiting our group for a month in May 2013.
2nd Austrian Computer Science Day
Sunday, Apr 21, 2013We 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 Widder
Thursday, Mar 21, 2013Josef 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, 2012Our 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, 2012Florian gave an interview about his research on bound computation to the Austrian daily newspaper “Der Standard”.
Joint Workshop between CMACS and RiSE in Washington, DC
Thursday, Sep 27, 2012Adjoint to the Austrian science talks in Washington, DC, our group participated in a joint workshop between CMACS and RiSE.
Ten funded PhD and PostDoc positions
Monday, Jul 9, 2012The 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 grant
Tuesday, Jun 26, 2012Florian 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 Weissenbacher
Tuesday, Jun 26, 2012Georg 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, 2012An 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, 2012The 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 Sokolova
Friday, Feb 24, 2012Ana 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ürnkranz
Thursday, Feb 23, 2012Johannes 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 25
Friday, Jan 13, 2012The 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 Clarke
Friday, Jan 13, 2012We 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, 2012The FORSYTE team is wishing our friends, colleagues and students a Happy New Year!
Winter School on Verification
Thursday, Dec 8, 2011The 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 Traunkirchen
Monday, Oct 10, 2011From 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 Engineering
Friday, May 28, 2010The 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, 2010The 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.