Cited in
(97)- Higher-order quantifier elimination, counter simulations and fault-tolerant systems
- Generalized rewrite theories, coherence completion, and symbolic methods
- RustHorn: CHC-based verification for Rust programs
- Regression verification for unbalanced recursive functions
- Constraint-based relational verification
- Code2Inv: a deep learning framework for program verification
- Automatic synthesis of logical models for order-sorted first-order theories
- Efficient Information-Flow Verification Under Speculative Execution
- Horn clause solvers for program verification
- An iterative approach to precondition inference using constrained Horn clauses
- An abstract domain of uninterpreted functions
- Incremental and modular context-sensitive analysis
- Software verification with PDR: an implementation of the state of the art
- Data abstraction: a general framework to handle program verification of data structures
- Compositional verification of smart contracts through communication abstraction
- Apron
- LOGEN
- FLATA
- DASWAM
- Aspic
- Dagger
- CDAOstore
- CPAchecker
- Ultimate Automizer
- TRACER
- UFO
- KRATOS
- PeRIPLO
- PhyloWS
- Interproc
- LLBMC
- Aligators
- Eldarica
- InvGen
- HMC
- ESBMC
- BitBlaze
- HSF
- InvA
- Mcmt
- Ciao
- CiaoPP
- Rex
- WebPIE
- PAGAI
- SymDiff
- OPTYap
- GNATprove
- YapOr
- IKOS
- ARMor
- AUSPICE-R
- OpenSMT2
- Spacer
- BOXES
- PKind
- CoVaC
- MoCHi
- DyTa
- CTIGAR
- SMACK
- VeriMAP
- PARLOG
- RAHFT
- April
- JayHorn
- HaLoop
- SAFARI
- Ultimate Taipan
- Yedalog
- Booster
- Crust
- Rust2Viper
- Manticore
- AIspace
- IncA
- Loop verification with invariants and contracts
- Concolic testing in CLP
- scientific article; zbMATH DE number 7453190 (Why is no real title available?)
- Partitioned memory models for program analysis
- Diffy
- Code2Inv
- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
- Leveraging compiler intermediate representation for multi- and cross-language verification
- solc-verify
- Pono
- CLN2INV
- A unifying view on SMT-based software verification
- Relational program reasoning using compiler IR
- Removing unnecessary variables from Horn clause verification conditions
- RustHorn
- AUSPICE-R: automatic safety-property proofs for realistic features in machine code
- VerX
- HolBA
- Jasmin
- Horn clause verification with convex polyhedral abstraction and tree automata-based refinement
- TreeAutomizer
This page was built for software: SeaHorn
