Institute for
Formal Models
and Verification

Organizing HWMCC'17 affiliated to FMCAD'17.

Our BMC paper from TACAS'99 received the
ETAPS'17 Test of Time Award.

March 1, 2017, Science Park 3, HS 19, 13:00 - 14:00
Sebastian Gabmeyer talks about
Symbolic Verification of Graph Transformation Systems
with Hardware Model Checkers

March 6, 2017, Science Park S2 Z74 13:00 - 14:00
Clifford Wolf talks about
Formal Verification of Verilog HDL with
Yosys-SMTBMC and SymbiYosys
followed by a discussion session from 14:00 - 15:00

Special issue of JAR on engineering aspects
of automated reasoning systems.
Submission deadline is 3 April 2017.
[ webpage | journal ]

Marijn Heule, University of Texas, Austin
Everything’s Bigger in Texas: The Largest Math Proof Ever
web page with lots of press coverage, related paper at SAT'16
June 22, 2016, 17:15 - 18:15, S3 HS18, Informatik, JKU

Talk by Priyank Kalla, Univ. Utah, on
Word-Level Abstractions from Digital Circuits
using Algebraic Geometry and Symbolic Computation
in our colloquium on March 16, 2016
08:30 - 09:30, S3 048, Informatik, JKU.

Armin Biere received the HVC'15 Award
for the most influential work in the last five years
in formal verification, simulation, and testing.

In our our doctoral college
Logical Methods in Computer Science (LogiCS)
and in our national research network RiSE
we have several open positions.

Organized HWMCC'15 affiliated to FMCAD'15.

We have a new major release for Boolector,
as well as minor updates for PicoSAT and Quantor.

Beside having organized 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.

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.

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

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

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.

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

Helping to organize QBF Gallery 2014.

We are organizing an advanced winter shool on
reasoning engines for rigorous system engineering.

Talk by Andrei Voronkov on
Solving Systems of Linear Inequalities
by Bound Propagation
in our colloquium on October 9, 2013
14:00 - 15:00, S3 055, Informatik.

Public appearance May 21st in 2013
(pictures, videos).