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 |
Samuel Bucheli Martin Brain Saurabh Joshi Pamela Farries Vojtech Forejt Daniel Kroening |
Meijia Ling Ashutosh Natraj Peter Schrammel Nassim Seghir Subodh Sharma Michael Tautschnig |
| PhD Students |
Leopold
Haller Alex Horn Alexander Kaiser David Landsberg Matt Lewis |
Lihao Liang Ganesh Narayanaswamy Vincent Nimal Daniel Poetzl Marcelo Sousa |
| 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, now at JP Morgan Gerard Basler, PhD ETH 2010, Thesis Nicolas Blanc, PhD ETH 2010, Thesis, now at Intel Georg Weissenbacher, PhD Oxford 2010, Thesis, now at TU Vienna 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 UCL Nannan He, now at Minnesota State University at Mankato Vijay Victor D'silva, PhD Oxford 2012, now at UCB Yury Chebiryak, PhD ETH Zürich 2012, Thesis Ajitha Rajan, now at the University of Edinburgh | |
Funding
