Institute for
Formal Models
and Verification

FLoC'14 Olympic Games

Beside organizing the
Hardware Model Checking Competition 2014 and the
QBF Gallery 2014 (presented at Vienna Summer of Logic)
our tools Lingeling, Boolector, and Demiurge (with TU Graz)
won several prizes at the SAT'14 Competition,
the SMT'14 Competition and at the first
Synthesis Competition 2014.

Open PhD Positions

In our new doctoral college
Logical Methods in Computer Science (LogiCS)
we have several openings
see also our FMV jobs page.

Most Influential Paper Award

Our BMC paper from TACAS'99 got the
most influential paper of 20 years of TACAS award.
We have separate page on Bounded Model Checking
with more information on the award.

Information Electronics Colloquium

Mo Movahed, Fahim Rahim, Hans-Jörg Peter
Atrenta – Early Design Closure using Formal Methods
Thursday, March 13, Science Park 1, MT 226, 08:30 - 10:00

TAP'14 Conference

Helping to organize 8th conference on
Tests & Proofs (TAP'14).

Hardware Model Checking Competition 2014
CAV'14 Edition

Organizing HWMCC'14 CAV Edition affiliated to CAV'14.
Part of FLoC Olympic Games at Vienna Summer of Logic 2014.
Results presented in second FLoC'14 Olympic Games ceremony.

CAV'14 Conference

Helping to organize 26th conference on
Computer Aided Verification (CAV'14)
part of Vienna Summer of Logic.

QBF Gallery 2014

Helping to organize QBF Gallery 2014.

ReRISE'14 Winter School

Colloquium

Talk by Andrei Voronkov on
Solving Systems of Linear Inequalities
by Bound Propagation

in our colloquium on October 9,
14:00 - 15:00, S3 055, Informatik.

Hardware Model Checking Competition 2013

Organized HWMCC'13 affiliated to FMCAD'13.

SAT Competition 2013

Lingeling, Plingeling, and Treengeling
awarded 7 medals: 4 gold, 3 silver.
Additional 3 medals in the
configuration challenge.

Donald Knuth
QBF 2013 Workshop

We are organizing the International Workshop on
Quantified Boolean Formulas 2013 QBF 2013
this July.

older events