The following pages link to Boogie (Q19731):
Displaying 50 items.
- Contract-based verification of MATLAB-style matrix programs (Q282101) (← links)
- Verification of object-oriented programs: a transformational approach (Q439944) (← links)
- Verification conditions for source-level imperative programs (Q465685) (← links)
- SMT-based model checking for recursive programs (Q518396) (← links)
- The dynamic frames theory (Q539422) (← links)
- Predicate abstraction in a program logic calculus (Q549686) (← links)
- Mechanical inference of invariants for FOR-loops (Q604381) (← links)
- Doomed program points (Q633286) (← links)
- Reasoning about memory layouts (Q633298) (← links)
- Software engineering and formal methods. 9th international conference, SEFM 2011, Montevideo, Uruguay, November 14--18, 2011. Proceedings (Q643151) (← links)
- Magic-sets for localised analysis of Java bytecode (Q656846) (← links)
- Verifying relative safety, accuracy, and termination for program approximations (Q682353) (← links)
- Proving mutual termination (Q746783) (← links)
- Checking data-race freedom of GPU kernels, compositionally (Q832190) (← links)
- Verified cryptographic code for everybody (Q832216) (← links)
- Product programs in the wild: retrofitting program verifiers to check information flow security (Q832225) (← links)
- Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms (Q832310) (← links)
- Proving fairness and implementation correctness of a microkernel scheduler (Q835766) (← links)
- Beyond contracts for concurrency (Q846113) (← links)
- Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18--21, 2008. Proceedings (Q955386) (← links)
- Automatic verification of Java programs with dynamic frames (Q973055) (← links)
- Integration of verification methods for program systems (Q1040327) (← links)
- An extensible encoding of object-oriented data models in HOL. With an application to IMP++ (Q1040775) (← links)
- Instrumenting a weakest precondition calculus for counterexample generation (Q1648649) (← links)
- Automating regression verification of pointer programs by predicate abstraction (Q1650864) (← links)
- Relational program reasoning using compiler IR (Q1703014) (← links)
- Unifying separation logic and region logic to allow interoperability (Q1798668) (← links)
- A FOOLish encoding of the next state relations of imperative programs (Q1799102) (← links)
- Assertion-based slicing and slice graphs (Q1941855) (← links)
- Stepwise refinement of heap-manipulating code in Chalice (Q1941869) (← links)
- A system for compositional verification of asynchronous objects (Q1951610) (← links)
- Alloy*: a general-purpose higher-order relational constraint solver (Q2009609) (← links)
- Automatic proofs of memory deallocation for a Whiley-to-C compiler (Q2058392) (← links)
- Verifying Whiley programs with Boogie (Q2102933) (← links)
- Generalized arrays for Stainless frames (Q2152661) (← links)
- A learning-based approach to synthesizing invariants for incomplete verification engines (Q2208307) (← links)
- First-order automated reasoning with theories: when deduction modulo theory meets practice (Q2209546) (← links)
- Safe functional systems through integrity types and verified assembly (Q2220814) (← links)
- Deductive verification of floating-point Java programs in KeY (Q2233510) (← links)
- Fifty years of Hoare's logic (Q2280214) (← links)
- Regression verification for unbalanced recursive functions (Q2281656) (← links)
- Exploiting pointer analysis in memory models for deductive verification (Q2287078) (← links)
- Verifying a concurrent garbage collector with a rely-guarantee methodology (Q2319995) (← links)
- Wombit: a portfolio bit-vector solver using word-level propagation (Q2323450) (← links)
- Program verification by coinduction (Q2324001) (← links)
- Automating deductive verification for weak-memory programs (Q2324213) (← links)
- A framework for the verification of certifying computations (Q2351144) (← links)
- On automation in the verification of software barriers: experience report (Q2351145) (← links)
- SMT proof checking using a logical framework (Q2441776) (← links)
- Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006) (Q2461559) (← links)
