Formal Verification
Summarised papers
- The existence of refinement mappings [abadi:tcs:1991]
- 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]
- Symbolic execution with separation logic [berdine:aplas:2005]
- Smallfoot: Modular automatic assertion checking with separation logic [berdine:fmco:2005]
- Permission accounting in separation logic [bornat:popl:2005]
- Compositional shape analysis by means of bi-abduction [calcagno:popl:2009]
- A precise yet efficient memory model for C [cohen:entcs:2009]
- End-to-end verification of information flow security for C and assembly programs [costanzo:pldi:2016]
- An abstract interpretation framework for refactoring with application to extract methods with contracts [cousot:oopsla:2012]
- Frama-C: A software analysis perspective [cuoq:sefm:2012]
- A local shape analysis based on separation logic [distefano:tacas:2006]
- Komodo: Using verification to disentangle secure-enclave hardware from software [ferraiuolo:sosp:2017]
- Multi-prover verification of C programs [filliatre:fem:2004]
- Specified blocks [hehner:vstte:2008]
- Fractional permissions without the fractions [heule:ftfjp:2011]
- The ramifications of sharing in data structures [hobor:popl:2013]
- VeriFast: A powerful, sound, predictable, fast verifier for C and Java [jacobs:nfm:2011]
- VeriFast: Imperative programs as proofs [jacobs:vstte:2010]
- RustBelt: Securing the foundations of the Rust programming language [jung:popl:2017]
- Verifying event-driven programs using ramified frame properties [krishnaswami:tldi: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]
- Verifying security invariants in ExpressOS [mai:asplos:2013]
- Formal verification of a memory allocation module of Contiki with Frama-C: a case study [mangano:crisis:2016]
- Boost the impact of continuous formal verification in industry [monteiro:arxiv:2019]
- TALx86: A realistic typed assembly language [morrisett:wcsss:1999]
- 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]
- Separation logic [ohearn:cacm:2019]
- Separation logic and abstraction [parkinson:popl:2005]
- 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]
- Separation logic: a logic for shared mutable data structures [reynolds:lics:2002]
- Lightweight support for magic wands in an automatic verifier [schwerhoff:ecoop:2015]
- Reasoning about a machine with local capabilities [skorstengaard:esop:2018]
- StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities [skorstengaard:popl:2019]
- Implicit dynamic frames: Combining dynamic frames and separation logic [smans:ecoop:2009]
- Alias types [smith:esop:2000]
- Scalable translation validation of unverified legacy OS code [tahat:fmcad:2019]
- 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
- Verification of TLB virtualization implemented in C [alkassar:vstte:2012]
- Cogent: Verifying high-assurance file system implementations [amani:asplos:2016]
- Large-scale formal verification in practice: A process perspective [andronick:icse:2012]
- The Spec# programming system: An overview [barnett:cassis:2004]
- The Spec# programming system: Challenges and directions [barnett:vstte:2005]
- A framework for cooperating decision procedures [barrett:cade:2000]
- Witnessing the elimination of magic wands [blom:ijsttt:2015]
- A semantics for concurrent separation logic [brookes:tcs:2006]
- A reachability predicate for analyzing low-level software [chatterjee:tacas:2007]
- The last mile: An empirical study of timing channels on seL4 [cock:ccs:2014]
- Unifying type checking and property checking for low-level code [condit:popl:2009]
- 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]
- Views: Compositional reasoning for concurrent programs [dinsdale-young:popl:2013]
- Locking discipline inference and checking [ernst:icse:2016]
- Static contract checking with abstract interpretation [fahndrich:foveoos:2010]
- Verification of a practical hardware security architecture through static information flow analysis [ferraiuolo:asplos:2017]
- 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]
- Ironclad apps: End-to-end security via automated full-system verification [hawblitzel:osdi:2014]
- Abstract read permissions: Fractional permissions without the fractions [heule:vmcai:2013]
- The VFiasco approach for a verified operating system [hohmuth:plos:2005]
- Applying source-code verification to a microkernel: the VFiasco project [hohmuth:sigops:2002]
- Dynamic frames: Support for framing, dependencies and sharing without restrictions [kassios:fm:2006]
- Machine assisted proof of ARMv7 instruction level isolation properties [khakpour:cpp:2013]
- SeL4: Formal verification of an OS kernel [klein:sosp:2009]
- 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]
- Specifying and verifying hardware for tamper-resistant software [lie:secpri:2003]
- Practical verification for the working programmer with CodeContracts and abstract interpretation [logozzo:vmcai:2011]
- Verified compilation on a verified processor [loow:pldi:2019]
- LLBMC: Bounded model checking of C and C++ programs using a compiler IR [merz:vstte:2012]
- Ynot: Dependent types for imperative programs [nanevski:icfp:2008]
- Specifying concurrent programs in separation logic: Morphisms and simulations [nanevski:oopsla:2019]
- RedLeaf: Towards an operating system for safe and verified firmware [narayanan:hotos:2019]
- Assertion-based encapsulation, object invariants and simulations [naumann:fmco:2004]
- Hyperkernel: Push-button verification of an OS kernel [nelson:sosp:2017]
- Resources, concurrency, and local reasoning [ohearn:tcs:2007]
- CIVL: the concurrency intermediate verification language [siegel:sc:2015]
- Push-button verification of file systems via crash refinement [sigurbjarnarson:osdi:2016]
- Heap-dependent expressions in separation logic [smans:fmood:2010]
- Growing solver-aided languages with Rosette [torlak:onward:2013]
- Establishing a refinement relation between binaries and abstract code [verbeek:fmmsd:2019]
- KRust: A formal executable semantics of Rust [wang:tase:2018]
- Safe to the last instruction: automated verification of a type-safe operating system [yang:pldi:2010]