swMATH18274MaRDI QIDQ30117FDOQ30117
Author name not available (Why is that?)
Official website: http://link.springer.com/chapter/10.1007/978-3-319-21690-4_20
Cited In (94)
- Diffy
- Code2Inv
- Efficient Information-Flow Verification Under Speculative Execution
- Incremental and modular context-sensitive analysis
- Title not available (Why is that?)
- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
- Removing unnecessary variables from Horn clause verification conditions
- RustHorn: CHC-based verification for Rust programs
- Higher-order quantifier elimination, counter simulations and fault-tolerant systems
- Generalized rewrite theories, coherence completion, and symbolic methods
- Regression verification for unbalanced recursive functions
- Constraint-based relational verification
- VerX
- Code2Inv: a deep learning framework for program verification
- HolBA
- Automatic synthesis of logical models for order-sorted first-order theories
- Jasmin
- Horn clause solvers for program verification
- An iterative approach to precondition inference using constrained Horn clauses
- An abstract domain of uninterpreted functions
- 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
- Concolic testing in CLP
- Loop verification with invariants and contracts
- Partitioned memory models for program analysis
- 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
- Leveraging compiler intermediate representation for multi- and cross-language verification
- solc-verify
- Pono
- CLN2INV
- RustHorn
- TreeAutomizer
- A unifying view on SMT-based software verification
- Relational program reasoning using compiler IR
- AUSPICE-R: automatic safety-property proofs for realistic features in machine code
- Horn clause verification with convex polyhedral abstraction and tree automata-based refinement
This page was built for software: SeaHorn
