Institute for
Formal Models
and Verification

Opening for full professorship at FMV

The Department of Computer Science at the Faculty of Engineering and Natural Sciences at Johannes Kepler University Linz invites applications for a permanent full-time position.
More information: https://www.jku.at/en/the-jku/work-at-the-jku/job-openings/professorship-positions/formal-methods/

GI Dissertation Prize 2020 for Daniela Kaufmann
Daniela Kaufmann received the GI Dissertation Prize 2020
awarded in 2021 for her PhD thesis jointly by the German (GI),
Austrian (OGC), and Swiss (SI) computer science associations.
LIT Lecture Series AI

Tuesday, November 3, 2020, 14:00 - 15:00, Cyberspace
Georg Gottlob Univ. Oxford and TU Wien
My adventures with Datalog:
Walking the thin line between theory and practice

in our Lecture Series Artificial Intelligence.

Hardware Model Checking Competition 2020

Organized HWMCC'20 affiliated to FMCAD'20
again with focus on BTOR2 word-level models.
Model checkers were due until September 1,
updates and benchmarks until September 8.
Results presented in HWMCC session of FMCAD'20.

Kissat in SAT Competition 2020

Our new SAT solver Kissat
won the first place in the main track of
the SAT Competition 2020.

LIT Lecture Series AI

Tuesday, January 21, 2020, 14:00 - 15:00, HS 1
Holger Hoos from the University of Leiden talks about
Addressing the AI Talent Bottleneck by Automating Artificial Intelligence
in our Lecture Series Artificial Intelligence.

Computer Science Colloquium

October 1, 2019, JKU Managment Zentrum
2nd floor, MZ 202B, 14:00 - 15:00
Günther Raidl from TU Wien talks about
Decision Diagrams in Combinatorial Optimization
in our colloquium

Hardware Model Checking Competition 2019

Organizing HWMCC'19 affiliated to FMCAD'19
focusing on word-level model checking of BTOR2 models.
Model checkers were due until September 28,
updates and benchmarks until October 13.

IJCAI-JAIR 2019 Award
Computer Science Colloquium

November 12, 2018, Science Park S3 055, 17:15 - 18:00
Radu Grosu talks about
Towards Explainable RNNs: Modeling, Learning and Verification
in our colloquium

Computer Science Colloquium

October 15, 2018, Science Park 3, 218, 12:00 - 12:45
Alan Mishchenko talks about
Integrating an AIG Package, Simulator and SAT Solver
in our colloquium

CAV 2018 Award

Received prestigious CAV 2018 Award.

Computer Science Colloquium

May 28, 2018, Science Park MT 127, 17:15 - 18:15
Warren A. Hunt Jr talks about
Specification and Verification of x86 Machine-Level Code
in our colloquium

Computer Science Colloquium

January 18, 2018, Science Park 3, 218, 10:15 - 11:00
Radu Mardare talks about
Quantitative Equational Reasoning
in our colloquium

Hardware Model Checking Competition 2017

Organizing HWMCC'17 affiliated to FMCAD'17.

ETAPS'17 Test of Time Award

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

Computer Science Colloquium

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
in our colloquium

Computer Science Colloquium

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

in our colloquium
followed by a discussion session from 14:00 - 15:00

JAR Special Issue on Automated Reasoning Systems

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

Computer Science Colloquium

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

Computer Science Colloquium
HVC'15 Award

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

Open PhD and Post-Doc Positions

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

Hardware Model Checking Competition 2015

Organized HWMCC'15 affiliated to FMCAD'15.

New Software Releases

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

FLoC'14 Olympic Games

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.

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, 2013
14:00 - 15:00, S3 055, Informatik.

Donald Knuth

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

older events

SAT Association vice-chair
FMCAD SC

JSAT editor
FMSD editor
JAIR associate editor
JAR editor

ATVA'21 PC
FDL'21 PC
CP'21 SPC
SAT'21 PC
CAV'21 PC
CPAIOR'21 PC
CADE'21 PC
TACAS'21 PC

HWMCC'20 organizer
FMCAD'20 PC
FDL'20 PC
ESA'20 PC
IJCAR'20 PC
TACAS'20 chair
IJCAI'20 PC
ADG'20 PC
SAT'20 chair
TACAS'20 artifact chair
ECAI'20 PC
QBFEval'20 organizer
SC2'20 PC
PAAR'20 PC
VMCAI'20 PC
AAAI'20 PC

ICTAI'19 SAT/CSP track PC
QBF'19 co-organizer
QBFEval'19 organizer
MODELS Demos'19 PC
Educators' Symposium'19 PC
MeTRiD'19 PC
SYNT'19 PC
IJCAI'19 PC
HWMCC'19 organizer
FMCAD'19 PC
FDL'19 PC
ARCADE'19 PC
SAT'19 PC
POS'19 PC
SMT'19 PC
NFM'19 PC
TACAS'19 PC
DATE'19 topic chair
AAAI'19 PC

MeTRiD'18 PC
IWIL'18 PC
ICTAI'18 SAT/CSP track PC
SYNASC'18 PC
WFLP'18 PC
ACM SRC'18 PC
FTSCS'18 PC
PC'18 PC
FMCAD'18 PC
IJCAI'18 PC
VST'18 PC
CAV'18 PC
POS'18 PC
QBFEVAL'18 co-organizer
QBF'18 co-organizer
TAP'18 PC
MODELS'18 PC
SAT'18 PC
IJCAR'18 PC
DATE'18 topic co-chair
TACAS'18 PC
AAAI'18 PC

HWMCC'17 organizer
ICTAI'17 SAT/CSP track PC
SMT'17 PC
HVC'17 PC
SYNASC'17 PC
MODELS'17 Demos PC
MODELS'17 EduSymp PC
MODELS'17 Posters PC
VOLT'17 PC
ACM-SRC'17 PC
SAT'17 PC
PoCR'17 PC
IJCAI'17 PC
QBFEVAL'17 co-organizer
ARCADE'17 PC
IWIL'17 PC
MODELS'17 PC
TAP'17 PC
FMCAD'17 PC
LPAR-21 PC
SPIN'17 PC
STAF'17 workshop co-chair
LATA'17 PC
TACAS'17 PC
DATE'17 topic co-chair
SOFSEM'17 PC
AAAI'17 PC

ICTAI'16 SAT/CSP track PC
VOLT'16 PC
MoDeVVa'16 PC
MODELS'16 SRC PC
MODELS'16 Demos PC
ME'16 PC
FTSCS'16 PC
COMMitMDE'16 PC
ACM-SRC'16 PC
HVC'16 PC
MEMICS'16 PC
AAAI'16 PC
ATVA'16 PC
IJCAI'16 PC
FMCAD'16 PC
SAT Workshop at Fields Institute organizer
QBF'16 organizer
POS'16 PC
PAAR'16 PC
SAT'16 PC
TAP'16 PC
MODELSWARD'16 PC
IJCAR'16 PC
DATE'16 PC
VMCAI'16 PC
VST'16 PC

IWIL'15 PC
PAS'15 PC
HVC'15 PC
LPAR-20 PC
ICTAI'15 SAT/CSP track PC
FMCAD'15 PC
HWMCC'15 organizer
SAT'15 PC
QBF'15 organizer
AVM'15 organizer
FFM'15 PC
TAP'15 PC
QUANTIFY'15 organizer
CAV'15 PC
SMT'15 PC
NFM'15 PC
Dagstuhl Seminar 15171 organizer
TACAS'15 PC
DATE'15 PC

HVC'14 PC
FTSCS'14 PC
ICTAI'14 SAT/CSP track PC
FMCAD'14 PC
TAP'14 chair
CAV'14 chair
HWMCC'14 CAV Edition organizer
SAT'14 PC
POS'14 PC
QBF Gallery 2014 organizer
NFM'14 PC
TACAS'14 PC
DATE'14 PC
BIRS Workshop organizer
ReRiSE'14 Winter School organizer

LPAR-19 PC
HVC'13 PC
ICTAI'13 SAT/CSP track PC
FTSCS'13 PC
HWMCC'13 organizer
FMCAD'13 PC
DIFTS'13 PC
QBF 2013 organizer
CAV'13 PC
SAT'13 PC
SPIN'13 PC
CPAIOR'13 PC
DATE'13 PC

older academic services