todo
https://en.wikipedia.org/wiki/Category:Model_checking
https://en.wikipedia.org/wiki/Widening_(computer_science)
Notes related to Model checking
BLAST verifier, Bounded model-checking, Büchi automaton, Case splitting, CPAchecker verifier, Kripke structure, Partial Order Reduction, SAT solver, State merging, Symbolic model checking, Temporal logic
Papers related to Model checking
- Automatic predicate abstraction of C programs [ball:pldi:2001]
- Model checking of C and C++ with DIVINE 4 [baranova:atva:2017]
- CPAchecker: A tool for configurable software verification [beyer:cav:2011]
- The software model checker BLAST: Applications to software engineering [beyer:ijsttt:2007]
- The BLAST query language for software verification [beyer:sas:2004]
- Symbolic model checking without BDDs [biere:tacas:1999]
- Code-level model checking in the software development workflow [chong:icse:2020]
- Model checking: Algorithmic verification and debugging [clarke:cacm:2009]
- Design and synthesis of synchronization skeletons using branching-time temporal logic [clarke:wlop:1982]
- Model checking boot code from AWS data centers [cook:cav:2018]
- Compositional may-must program analysis: Unleashing the power of alternation [godefroid:popl:2010]
- Software verification with BLAST [henzinger:spin:2003]
- Swarm verification techniques [holzmann:ieeetse:2011]
- Software model checking [jhala:compsurv:2009]
- The human in formal methods [krishnamurthi:fm:2019]
- Sanity checks in formal verification [kupferman:concur:2006]
- DAG inlining: A decision procedure for reachability-modulo-theories in hierarchical programs [lal:pldi:2015]
- Verification of an implementation of Tomasulo's algorithm by compositional model checking [mcmillan:cav:1998]
- Model checking [mcmillan:ecs:2003]
- The temporal logic of programs [pnueli:sfcs:1977]
- Defining interfaces between hardware and software: Quality and performance [reid:phd:2019]
- Relational test tables: A practical specification language for evolution and security [weigl:arxiv:2019]