| Personals |
Publications,
DBLP,
Google Scholar,
ORCID,
Semantic Scholar
Biographical sketch
Curriculum vitae
You can also follow me on Twitter and
Google+.
|
| NEW |
Domain-Independent Multi-threaded Software Model Checking (ASE 2018)
CPA-SymExec: Efficient Symbolic Execution in CPAchecker (ASE 2018)
Keynote at TAP 2018
Tests from Witnesses: Execution-Based Validation of Verification Results (TAP 2018)
A Unifying View on SMT-Based Software Verification (J. Autom. Reasoning 2018)
Reducer-Based Construction of Conditional Verifiers (ICSE 2018)
Combining Model Checking and Data-Flow Analysis (Handbook of Model Checking 2018)
Software Verification: Testing vs. Model Checking (HVC 2017)
Software Verification with Validation of Results (TACAS 2017)
|
|
Research |
My research focuses
on models, algorithms, and tools for the
construction and analysis of reliable software systems, in particular:
Interfaces for component-based design (download Chic)
Software model checking and static analysis (download CPAchecker,
BLAST,
CSIsat)
Structure analysis and comprehension of large systems
(download CrocoPat or CCVisu)
Formal verification of real-time systems (download Rabbit) |
| Service |
PC Chair: TAP 2019 (Oct 7-11, 2019, Porto, Portugal)
8th Intl. TACAS Competition on Software Verification (SV-COMP'19)
PC Chair: TACAS 2018
1st Intl. Workshop on CPAchecker (CPA'16)
CAV 2015 Workshops
Program committees:
ICSME'15,
TAP'15,
ICPC'15,
FMSPLE'15,
NFM'15,
SPIN'14,
FMCAD'14,
FORTE'14
... more
|
Teaching
|
Courses offered: current term,
next term
... more
|
| People |
Team
Information for prospective students
Technical hints for writing a paper
Software that I use
|
| Software |
BenchExec: Reliable Benchmarking and Resource Measurement
BLAST: Model Checking of Software
CCVisu: Visual Clustering and Software-Structure Assessment
CheckDep: Tracking Software Dependencies
Chic: Checking Interface Compatibility
CPAchecker: Configurable Software Verification
CrocoPat: Relational Programming
(for Software-Structure Analysis)
CSIsat: Interpolation for LA+EUF
DepDigger: Detecting Complex Low-Level Dependencies
JavaSMT: A Unified Interface for SMT Solvers in Java
Rabbit: Verification of Real-Time Systems
... more
|
