The following pages link to KRAKATOA (Q15691):
Displayed 50 items.
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program (Q352952) (← links)
- JCML: A specification language for the runtime verification of Java card programs (Q436381) (← links)
- Verification conditions for source-level imperative programs (Q465685) (← links)
- A dynamic logic for deductive verification of multi-threaded programs (Q470007) (← links)
- Automatic decidability and combinability (Q549666) (← links)
- Modular inference of subprogram contracts for safety checking (Q604392) (← links)
- Doomed program points (Q633286) (← links)
- Reasoning about memory layouts (Q633298) (← links)
- Product programs in the wild: retrofitting program verifiers to check information flow security (Q832225) (← links)
- Proving fairness and implementation correctness of a microkernel scheduler (Q835766) (← links)
- CPBPV: a constraint-programming framework for bounded program verification (Q968353) (← links)
- Instrumenting a weakest precondition calculus for counterexample generation (Q1648649) (← links)
- Understanding parameters of deductive verification: an empirical investigation of KeY (Q1791175) (← links)
- Weakest pre-condition reasoning for Java programs with JML annotations (Q1881666) (← links)
- The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML (Q1881670) (← links)
- Formal verification of numerical programs: from C annotated programs to mechanical proofs (Q1949765) (← links)
- TASS: the toolkit for accurate scientific software (Q1949767) (← links)
- FEVS: a functional equivalence verification suite for high-performance scientific computing (Q1949768) (← links)
- A system for compositional verification of asynchronous objects (Q1951610) (← links)
- Verifying Whiley programs with Boogie (Q2102933) (← links)
- Deductive verification of floating-point Java programs in KeY (Q2233510) (← links)
- Exploiting pointer analysis in memory models for deductive verification (Q2287078) (← links)
- A framework for the verification of certifying computations (Q2351144) (← links)
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) (Q2351415) (← links)
- Trusting computations: a mechanized proof from partial differential equations to actual program (Q2398899) (← links)
- Formal verification of side-channel countermeasures using self-composition (Q2442950) (← links)
- A program logic for resources (Q2463560) (← links)
- A proof outline logic for object-oriented programming (Q2571207) (← links)
- Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts (Q2642466) (← links)
- Are the logical foundations of verifying compiler prototypes matching user expectations? (Q2643125) (← links)
- Specification and verification challenges for sequential object-oriented programs (Q2643131) (← links)
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler (Q2655335) (← links)
- Viper: A Verification Infrastructure for Permission-Based Reasoning (Q2796035) (← links)
- Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach (Q2802468) (← links)
- Behavioral interface specification languages (Q2875082) (← links)
- Practical Realisation and Elimination of an ECC-Related Software Bug Attack (Q2890003) (← links)
- Automating Induction with an SMT Solver (Q2891425) (← links)
- Reasoning about Assignments in Recursive Data Structures (Q2999318) (← links)
- Verification of the Schorr-Waite Algorithm – From Trees to Graphs (Q3003486) (← links)
- Correct Code Containing Containers (Q3012966) (← links)
- Dafny: An Automatic Program Verifier for Functional Correctness (Q3066108) (← links)
- Matching Logic: An Alternative to Hoare/Floyd Logic (Q3067473) (← 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)
- Hardware-Dependent Proofs of Numerical Programs (Q3100216) (← links)
- Practical Tactics for Separation Logic (Q3183539) (← links)
- An Introduction to Certificate Translation (Q3184785) (← links)
- A Hoare Logic for Call-by-Value Functional Programs (Q3521994) (← links)
- Imperative Functional Programming with Isabelle/HOL (Q3543655) (← links)