Boogie

swMATH7714MaRDI QIDQ19731

No author found.

Related Items (only showing first 100 items - show all)

Verifying Catamorphism-Based Contracts using Constrained Horn Clauses ⋮ Contract-based verification of MATLAB-style matrix programs ⋮ Proving the Safety of Highly-Available Distributed Objects ⋮ Unnamed Item ⋮ Splitting via Interpolants ⋮ Automating Induction with an SMT Solver ⋮ Decision Procedures for Region Logic ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Checking data-race freedom of GPU kernels, compositionally ⋮ Verified cryptographic code for everybody ⋮ Product programs in the wild: retrofitting program verifiers to check information flow security ⋮ Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms ⋮ Zeno: An Automated Prover for Properties of Recursive Data Structures ⋮ Proving fairness and implementation correctness of a microkernel scheduler ⋮ The Relationship Between Separation Logic and Implicit Dynamic Frames ⋮ Combining Model Checking and Testing ⋮ Time Bounds for General Function Pointers ⋮ Beyond contracts for concurrency ⋮ Reasoning About Loops Using Vampire in KeY ⋮ Severity Levels of Inconsistent Code ⋮ Two for the Price of One: Lifting Separation Logic Assertions ⋮ Generalized arrays for Stainless frames ⋮ Instrumenting a weakest precondition calculus for counterexample generation ⋮ Specification and verification challenges for sequential object-oriented programs ⋮ Automating regression verification of pointer programs by predicate abstraction ⋮ Principled Software Development ⋮ Faster and more complete extended static checking for the Java modeling language ⋮ HOL-Boogie -- an interactive prover-backend for the verifying C compiler ⋮ Mechanical inference of invariants for FOR-loops ⋮ Horn Clause Solvers for Program Verification ⋮ Automated Algebraic Reasoning for Collections and Local Variables with Lenses ⋮ Assertion-based slicing and slice graphs ⋮ Stepwise refinement of heap-manipulating code in Chalice ⋮ Matching Multiplications in Bit-Vector Formulas ⋮ Conjunctive Abstract Interpretation Using Paramodulation ⋮ Doomed program points ⋮ Reasoning about memory layouts ⋮ Relational program reasoning using compiler IR ⋮ A system for compositional verification of asynchronous objects ⋮ Verification of object-oriented programs: a transformational approach ⋮ A learning-based approach to synthesizing invariants for incomplete verification engines ⋮ Encoding Monomorphic and Polymorphic Types ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ Software engineering and formal methods. 9th international conference, SEFM 2011, Montevideo, Uruguay, November 14--18, 2011. Proceedings ⋮ SMT proof checking using a logical framework ⋮ Verification conditions for source-level imperative programs ⋮ Safe functional systems through integrity types and verified assembly ⋮ Modular Verification of Procedure Equivalence in the Presence of Memory Allocation ⋮ Magic-sets for localised analysis of Java bytecode ⋮ HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier ⋮ The Relationship between Separation Logic and Implicit Dynamic Frames ⋮ Compositionality Entails Sequentializability ⋮ Deductive verification of floating-point Java programs in KeY ⋮ Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006) ⋮ A Polymorphic Intermediate Verification Language: Design and Logical Encoding ⋮ Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions ⋮ Verifying relative safety, accuracy, and termination for program approximations ⋮ SMT-based model checking for recursive programs ⋮ Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18--21, 2008. Proceedings ⋮ The dynamic frames theory ⋮ Alloy*: a general-purpose higher-order relational constraint solver ⋮ Inferring Loop Invariants Using Postconditions ⋮ Automatic verification of Java programs with dynamic frames ⋮ Predicate abstraction in a program logic calculus ⋮ Automated Verification of Practical Garbage Collectors ⋮ A Machine Checked Soundness Proof for an Intermediate Verification Language ⋮ SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities ⋮ Predicate Abstraction in a Program Logic Calculus ⋮ Fifty years of Hoare's logic ⋮ Regression verification for unbalanced recursive functions ⋮ Viper: A Verification Infrastructure for Permission-Based Reasoning ⋮ Dafny: An Automatic Program Verifier for Functional Correctness ⋮ Static Contract Checking with Abstract Interpretation ⋮ A Refinement Methodology for Object-Oriented Programs ⋮ A Dynamic Logic for Unstructured Programs with Embedded Assertions ⋮ Exploiting pointer analysis in memory models for deductive verification ⋮ Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach ⋮ A Basis for Verifying Multi-threaded Programs ⋮ Unifying separation logic and region logic to allow interoperability ⋮ A FOOLish encoding of the next state relations of imperative programs ⋮ ExplainHoudini: Making Houdini Inference Transparent ⋮ Proving mutual termination ⋮ Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories ⋮ Automatic proofs of memory deallocation for a Whiley-to-C compiler ⋮ A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic ⋮ Verifying a concurrent garbage collector with a rely-guarantee methodology ⋮ Wombit: a portfolio bit-vector solver using word-level propagation ⋮ Program verification by coinduction ⋮ Shape Analysis of Low-Level C with Overlapping Structures ⋮ Considerate Reasoning and the Composite Design Pattern ⋮ Automating deductive verification for weak-memory programs ⋮ Integration of verification methods for program systems ⋮ An extensible encoding of object-oriented data models in HOL. With an application to IMP++ ⋮ Invariants Synthesis over a Combined Domain for Automated Program Verification ⋮ Verifying Whiley programs with Boogie ⋮ A framework for the verification of certifying computations ⋮ On automation in the verification of software barriers: experience report ⋮ Behavioral interface specification languages ⋮ Verifiable Code Generation from Scheduled Event-B Models

This page was built for software: Boogie