FORSYTE alumni Marcel Moosbrugger graduated with the highest possible distinction for academic achievements (Promotio sub auspiciis Praesidentis). Congratulations! Find out more about the ceremony here.

The FORSYTE group mourns the death of Anna Prianichnkova, our beloved colleague and friend. Anna was the wife of the late Prof. Helmut Veith (the founder of the FORSYTE research group), and the coordinator of several doctoral colleges the FORSYTE group is involved in. Anna will be missed dearly. Obituary of VCLA (by Stefan Szeider and Agata Ciabattoni Obituary of the Faculty of Informatics (by Georg Weissenbacher)

The stipend is awarded to motivated female computer science students pursuing a master’s program in English. Find out more about the award and the upcoming ceremony here.

We 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).

The 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!

Lea 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 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. Read more here. ```

Abenteuer Informatik, initiated by FORSYTE members in 2022, was featured in the online edition of Der Standard. Read the article here.

Petra 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 has successfully defended her PhD thesis titled "Towards Automating Induction for Software Verification Guiding Inductive Reasoning in Superposition-based Theorem Proving". Congratulations!

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!

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 received the Best Paper Award at FORTE21 for their Case Study on Parametric Verification of Failure Detectors. Congratulations!

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.

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”.

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!

We welcome Pavol Černý, who joins the FORSYTE group as a full professor of computer science in September 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

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 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!

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!

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.

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.

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!

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).

We have a great program at FRIDA’17 that takes place in Vienna

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.

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.

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.

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.

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!

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 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

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

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ć 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!

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.

We had nice talks at the workshop on Formal Reasoning in Distributed Algorithms (FRIDA) this year. Look at the workshop web page.

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.

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.

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

Josef Widder and Igor Konnov are co-organizing the third workshop on Formal Reasoning in Distributed Algorithms. Check the workshop page.

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.

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.

Annu Gmeiner defended her PhD thesis on parameterized verification of fault-tolerant distributed algorithms. Congratulations!

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 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.

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.

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).

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

Josef Widder has received his habilitation in computer science from TU Wien. He is now Privatdozent.

We had great talks at FRIDA’15 workshop in Grenoble. The slides of some of the talks are available online.

Check 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 “PRAVDA” on Parameterized Verification of Fault-tolerant Distributed Algorithms

iDQ v1.0 is now available online: http://forsyte.at/software/idq/

We have a great program for our workshop on formal reasoning in distributed algorithms. Join us at the workshop!

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.

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.

Josef Widder is invited to talk tomorrow at Imagine 14 about how research funding started his IT career.

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 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.

Igor Konnov and Josef Widder are organizing the CAV Workshop FRIDA.

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.

The new version 0.9.3 of CBMC-GC is now available online: http://forsyte.at/software/cbmc-gc/

FWF has approved a doctoral college for Logical Methods in Computer Science. Details are available on the LogiCS website.

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.

Our group is coorganizing the Vienna Summer of Logic, the largest conference in the history of logic. http://vsl2014.at

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/

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=

Andi Holzer successfully defended his PhD thesis.

Aaron Bradley is visiting our group for June 2013, and teaching a course on IC3.

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 is visiting our group for a month in May 2013.

We are co-organizing the Austrian Computer Science Day 2013 at IST Austria. http://ist.ac.at/austrian-computer-science-day-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.

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 gave an interview about his research on bound computation to the Austrian daily newspaper “Der Standard”.

Adjoint to the Austrian science talks in Washington, DC, our group participated in a joint workshop between CMACS and RiSE.

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 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

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”.

http://www.informatiktag.at/

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

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.

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————————–

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

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.

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

The FORSYTE team is wishing our friends, colleagues and students a Happy New Year!

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.

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):

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.

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.