Quick Links
- Daniel Kroening
- Boolean Programs
- SMT Lists/Sets/Maps
- Google groups:
- SMT 2010
Systems Verification Group
About us
We are interested in formal methods for the correct construction of hardware
and software systems. Our focus is on automated methods
for checking compliance of an implementation with a specification,
and in particular Model Checking.
We are particularily interested in applying these methods to practical hardware and software implementations given in industrial languages such as Verilog, C or C++. Read more about software verification or hardware verification.
Loading...
NEW: We are hiring Postdocs and PhD students!
Recent Publications
- NEW Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs
- NEW Linear Completeness Thresholds for Bounded Model Checking
- NEW Test-Case Generation for Embedded Simulink via Formal Concept Analysis
- NEW Loop Summarization and Termination Analysis
- Termination Analysis with Compositional Transition Invariants
Group Members
| Staff |
Martin Brain Daniel Kroening Ajitha Ranjan |
Nassim Seghir Subodh Sharma Michael Tautschnig |
| PhD Students |
Yury Chebiryak Leopold Haller Alex Horn Alexander Kaiser |
David Landsberg Matt Lewis Lihao Liang Ganesh Narayanaswamy Vincent Nimal |
| MSc Students | ||
| Alumni |
Igor Zinovik, Postdoc Thomas Witkowski, MSc 2007, Thesis Samuel Bernet, MSc 2008 Raphael Mack, MSc 2008, Thesis Thomas Lenherr, MSc 2008, Thesis Sean Heelan, MSc 2009, Thesis, Hoare Project Prize Haoxian Zhao, MSc 2009, Thesis Gerard Basler, PhD ETH 2010, Thesis Nicolas Blanc, PhD ETH 2010, Thesis, now at Intel Georg Weissenbacher, PhD Oxford 2010, Thesis, now in Princeton Mitra Purandare, PhD ETH 2010, Thesis, now at IBM Philipp Ruemmer, now Assistant Professor in Uppsala Christoph Wintersteiger, PhD ETH 2011, Thesis, now at Microsoft Research Angelo Brillout, PhD ETH 2011, Thesis Thomas Wahl, now at Northeastern University, Boston Alastair Donaldson, now at Imperial College Jade Alglave, now at Queen Mary Nannan He, now at Advanced Digital Sciences Center, Singapore Vijay Victor D'silva, PhD Oxford 2012, now at UCB | |
Funding
