Tools
Summarised papers
- Verifying constant-time implementations [almeida:security:2016]
- Leveraging Rust types for modular specification and verification [astrauskas:oopsla:2019]
- Verifying Rust programs with SMACK [baranowski:atva:2018]
- Specification and verification: The Spec# experience [barnett:cacm:2011]
- Boogie: A modular reusable verifier for object-oriented programs [barnett:fmco:2005]
- Smallfoot: Modular automatic assertion checking with separation logic [berdine:fmco:2005]
- Compositional shape analysis by means of bi-abduction [calcagno:popl:2009]
- A precise yet efficient memory model for C [cohen:entcs:2009]
- Frama-C: A software analysis perspective [cuoq:sefm:2012]
- SecChisel: Language and tool for practical and scalable security verification of security-aware hardware architectures [deng:hasp:2019]
- A local shape analysis based on separation logic [distefano:tacas:2006]
- Multi-prover verification of C programs [filliatre:fem:2004]
- Specified blocks [hehner:vstte:2008]
- Fractional permissions without the fractions [heule:ftfjp:2011]
- VeriFast: A powerful, sound, predictable, fast verifier for C and Java [jacobs:nfm:2011]
- VeriFast: Imperative programs as proofs [jacobs:vstte:2010]
- A solver for reachability modulo theories [lal:cav:2012]
- The Boogie verification debugger [legoues:sefm:2011]
- Verification of concurrent programs with Chalice [leino:fosad:2007]
- Developing verified programs with Dafny [leino:icse:2013]
- Dafny: An automatic program verifier for functional correctness [leino:lpair:2010]
- No panic! Verification of Rust programs by symbolic execution [lindner:indin:2018]
- Formal verification of a memory allocation module of Contiki with Frama-C: a case study [mangano:crisis:2016]
- Viper: A verification infrastructure for permission-based reasoning [muller:vmcai:2016]
- Scaling symbolic evaluation for automated verification of systems code with Serval [nelson:sosp:2019]
- Sound formal verification of Linux's USB BP keyboard driver [penninckx:nfm:2012]
- Software verification with VeriFast: Industrial case studies [philippaerts:scp:2014]
- SMACK: Decoupling source language details from verifier implementations [rakamaric:cav:2014]
- Lightweight support for magic wands in an automatic verifier [schwerhoff:ecoop:2015]
- Implicit dynamic frames: Combining dynamic frames and separation logic [smans:ecoop:2009]
- Crust: A bounded verifier for Rust [toman:ase:2015]
- A lightweight symbolic virtual machine for solver-aided host languages [torlak:pldi:2014]
- Local reasoning about while-loops [tuerk:vstte:2010]
- Annotation inference for separation logic based verifiers [vogels:fmoods:2011]
- -Overify: Optimizing programs for fast verification [wagner:hotos:2013]
- SpaceSearch: A library for building and verifying solver-aided tools [weitz:icfp:2017]
Unsummarised papers
- The Spec# programming system: An overview [barnett:cassis:2004]
- The Spec# programming system: Challenges and directions [barnett:vstte:2005]
- Witnessing the elimination of magic wands [blom:ijsttt:2015]
- A reachability predicate for analyzing low-level software [chatterjee:tacas:2007]
- Model checking boot code from AWS data centers [cook:cav:2018]
- Enforcing high-level protocols in low-level software [deline:pldi:2001]
- The Lean theorem prover (system description) [demoura:cade:2015]
- Z3: An efficient SMT solver [demoura:tacas:2008]
- Locking discipline inference and checking [ernst:icse:2016]
- Static contract checking with abstract interpretation [fahndrich:foveoos:2010]
- The Why/Krakatoa/Caduceus platform for deductive program verification [filliatre:cav:2007]
- Why3 — where programs meet provers [filliatre:esop:2013]
- CSeq: a concurrency pre-processor for sequential C verification tools [fischer:ase:2013]
- The SeaHorn verification framework [gurfinkel:cav:2015]
- Behavioral interface specification languages [hatcliff:compsurv:2012]
- Powering the static driver verifier using Corral [lal:fse:2014]
- Reasoning about comprehensions with first-order SMT solvers [leino:sac:2009]
- A polymorphic intermediate verification language: Design and logical encoding [leino:tacas:2010]
- Practical verification for the working programmer with CodeContracts and abstract interpretation [logozzo:vmcai:2011]
- LLBMC: Bounded model checking of C and C++ programs using a compiler IR [merz:vstte:2012]
- Hyperkernel: Push-button verification of an OS kernel [nelson:sosp:2017]
- CIVL: the concurrency intermediate verification language [siegel:sc:2015]
- Heap-dependent expressions in separation logic [smans:fmood:2010]
- Growing solver-aided languages with Rosette [torlak:onward:2013]
- Safe to the last instruction: automated verification of a type-safe operating system [yang:pldi:2010]