The following pages link to Boogie (Q19731):
Displaying 50 items.
- Specification and verification challenges for sequential object-oriented programs (Q2643131) (← links)
- Faster and more complete extended static checking for the Java modeling language (Q2655328) (← links)
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler (Q2655335) (← links)
- Automated Verification of Practical Garbage Collectors (Q2786120) (← links)
- Viper: A Verification Infrastructure for Permission-Based Reasoning (Q2796035) (← links)
- Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach (Q2802468) (← links)
- A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic (Q2830009) (← links)
- Invariants Synthesis over a Combined Domain for Automated Program Verification (Q2842643) (← links)
- Behavioral interface specification languages (Q2875082) (← links)
- Splitting via Interpolants (Q2891411) (← links)
- Automating Induction with an SMT Solver (Q2891425) (← links)
- Decision Procedures for Region Logic (Q2891431) (← links)
- Zeno: An Automated Prover for Properties of Recursive Data Structures (Q2894285) (← links)
- The Relationship Between Separation Logic and Implicit Dynamic Frames (Q2904617) (← links)
- Two for the Price of One: Lifting Separation Logic Assertions (Q2914243) (← links)
- Horn Clause Solvers for Program Verification (Q2947164) (← links)
- Matching Multiplications in Bit-Vector Formulas (Q2961559) (← links)
- Conjunctive Abstract Interpretation Using Paramodulation (Q2961582) (← links)
- Encoding Monomorphic and Polymorphic Types (Q2974796) (← links)
- (Q2979818) (← links)
- (Q2979840) (← links)
- (Q2981009) (← links)
- Modular Verification of Procedure Equivalence in the Presence of Memory Allocation (Q2988675) (← links)
- The Relationship between Separation Logic and Implicit Dynamic Frames (Q3000593) (← links)
- Compositionality Entails Sequentializability (Q3000634) (← links)
- Dafny: An Automatic Program Verifier for Functional Correctness (Q3066108) (← links)
- Static Contract Checking with Abstract Interpretation (Q3067530) (← links)
- A Refinement Methodology for Object-Oriented Programs (Q3067544) (← links)
- A Dynamic Logic for Unstructured Programs with Embedded Assertions (Q3067545) (← links)
- ExplainHoudini: Making Houdini Inference Transparent (Q3075491) (← links)
- Combining Model Checking and Testing (Q3176377) (← links)
- Time Bounds for General Function Pointers (Q3178280) (← links)
- Reasoning About Loops Using Vampire in KeY (Q3460073) (← links)
- Severity Levels of Inconsistent Code (Q3460549) (← links)
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier (Q3543656) (← links)
- A Polymorphic Intermediate Verification Language: Design and Logical Encoding (Q3557085) (← links)
- Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions (Q3558212) (← links)
- Inferring Loop Invariants Using Postconditions (Q3586008) (← links)
- A Machine Checked Soundness Proof for an Intermediate Verification Language (Q3599104) (← links)
- SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities (Q3600478) (← links)
- Predicate Abstraction in a Program Logic Calculus (Q3605465) (← links)
- A Basis for Verifying Multi-threaded Programs (Q3617715) (← links)
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories (Q3636870) (← links)
- Shape Analysis of Low-Level C with Overlapping Structures (Q3656885) (← links)
- Considerate Reasoning and the Composite Design Pattern (Q3656894) (← links)
- Principled Software Development (Q4558903) (← links)
- Verifying Catamorphism-Based Contracts using Constrained Horn Clauses (Q5038461) (← links)
- Proving the Safety of Highly-Available Distributed Objects (Q5041111) (← links)
- Automated Algebraic Reasoning for Collections and Local Variables with Lenses (Q5098716) (← links)
- Verification of Concurrent Systems with VerCors (Q5175776) (← links)
