• Home

The 2nd Winter School in Computer Science & Engineering on Formal Verification

General Director: Michael Rabin

Event date: December 17 - December 21, 2017

    Moshe Vardi (Rice University)
    Orna Kupferman (The Hebrew University)




    Safety-critical computers increasingly affect nearly every aspect of our lives. Computers control the planes we fly on, monitor our health in hospitals and do our work in hazardous environments.  Computers with software deficiencies have resulted in catastrophic failures. The goal of formal verification is to to improve the safety and reliability of such hardware and software systems.

    Formal Verification is the study of algorithms and structures applicable to the verification of hardware and software designs.  It draws upon ideas and results from logic, graph theory, and automata theory, and combines theoretical and experimental aspects. While 30 years ago this was a subject of academic interest only, today, many companies use formal verification as an integral part of the development process.

    The IIAS Winter School on Formal Verification would bring together several leading researchers to cover the mathematicall and algorithmic foundations of the field, as well as to discuss its application in industry, and its impact on related areas in computer science.


    Confirmed Speakers:

    Rabin Lecture: Thomas A. Henzinger, IST


    Christel Baier, TU Dresden: Probabilistic verification
    Javier Esparza, TU Munich : Linear-time verification
    Bernd Finbeiner, University of Saarland : Temporal synthesis
    Orna Grumberg, The Technion: SAT-based verification

    Formal verification in related-areas panel:
    Danny Dolev, The Hebrew University: Cybersecurity
    David Harel, Weizmann: Computational Biology
    Noam Nissan, The Hebrew University: Algorithmic Game Theory

    Industrial Formal Verification Panel:

    Shirit Schvartzblat,  Mellanox

    Cindy Eisner, IBM

    Gila Kamhi, GM


    Moshe Vardi: From Aristotle to the iPhone