SeaHorn

swMATH18274MaRDI QIDQ30117FDOQ30117

Author name not available (Why is that?)

Cited In (26)

• 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
• 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
• Concolic testing in CLP
• Loop verification with invariants and contracts
• Title not available (Why is that?)
• Partitioned memory models for program analysis
• Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
• Leveraging compiler intermediate representation for multi- and cross-language verification
• A unifying view on SMT-based software verification
• Relational program reasoning using compiler IR
• Removing unnecessary variables from Horn clause verification conditions
• 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