KRAKATOA
From MaRDI portal
Cited in
(only showing first 100 items - show all)- ZB 2005: Formal Specification and Development in Z and B
- Trusting computations: a mechanized proof from partial differential equations to actual program
- Static contract checking with abstract interpretation
- Verification conditions for source-level imperative programs
- A dynamic logic for deductive verification of multi-threaded programs
- A verifying compiler for a multi-threaded object-oriented language
- Theorem Proving in Higher Order Logics
- Understanding parameters of deductive verification: an empirical investigation of KeY
- JCML: A specification language for the runtime verification of Java card programs
- Correct code containing containers
- The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
- Specification and runtime verification of Java card programs
- Could We Have Chosen a Better Loop Invariant or Method Contract?
- Local reasoning for global invariants. II: Dynamic boundaries
- Doomed program points
- Reasoning about memory layouts
- Weakest pre-condition reasoning for Java programs with JML annotations
- Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes
- Exploiting pointer analysis in memory models for deductive verification
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- A system for compositional verification of asynchronous objects
- CPBPV: a constraint-programming framework for bounded program verification
- Proving Correctness and Security of Two-Party Computation Implemented in Java in Presence of a Semi-honest Sender
- FEVS: a functional equivalence verification suite for high-performance scientific computing
- Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Practical Tactics for Separation Logic
- Verification of Java Programs with Generics
- One logic to use them all
- Multi-prover verification of floating-point programs
- An Introduction to Certificate Translation
- Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts
- Specification and verification challenges for sequential object-oriented programs
- A refinement methodology for object-oriented programs
- Semi-persistent Data Structures
- Theorem Proving in Higher Order Logics
- Proving fairness and implementation correctness of a microkernel scheduler
- Practical realisation and elimination of an ECC-related software bug attack
- A proof outline logic for object-oriented programming
- Dafny: an automatic program verifier for functional correctness
- A dynamic logic for unstructured programs with embedded assertions
- MUNCH -- automated reasoner for sets and multisets
- Verification of the Schorr-Waite algorithm -- from trees to graphs
- TASS: the toolkit for accurate scientific software
- A Machine Checked Soundness Proof for an Intermediate Verification Language
- Formal verification of numerical programs: from C annotated programs to mechanical proofs
- A Hoare Logic for Call-by-Value Functional Programs
- Towards Modular Algebraic Specifications for Pointer Programs: A Case Study
- Verification, Model Checking, and Abstract Interpretation
- Inferring Loop Invariants Using Postconditions
- Verifying Whiley programs with Boogie
- Product programs in the wild: retrofitting program verifiers to check information flow security
- Imperative Functional Programming with Isabelle/HOL
- scientific article; zbMATH DE number 7566072 (Why is no real title available?)
- Formal verification of side-channel countermeasures using self-composition
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- Automating Induction with an SMT Solver
- A Certified Lightweight Non-interference Java Bytecode Verifier
- Algebraic Methodology and Software Technology
- Deductive verification of floating-point Java programs in KeY
- Abstract Interpretation of Symbolic Execution with Explicit State Updates
- LCF-style Platform based on Multiway Decision Graphs
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- A framework for the verification of certifying computations
- Viper: a verification infrastructure for permission-based reasoning
- Matching logic: an alternative to Hoare/Floyd logic
- Fundamental Approaches to Software Engineering
- Automatic decidability and combinability
- A program logic for resources
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System
- Typed Lambda Calculi and Applications
- Hardware-Dependent Proofs of Numerical Programs
- Combining Coq and Gappa for Certifying Floating-Point Programs
- Are the logical foundations of verifying compiler prototypes matching user expectations?
- Complete instantiation-based interpolation
- Modular inference of subprogram contracts for safety checking
- Instrumenting a weakest precondition calculus for counterexample generation
- Reasoning about assignments in recursive data structures
- Behavioral interface specification languages
- Grail
- HOL-Boogie
- KeY-C
- LARCH
- TVOC
- SPARK
- Eiffel
- ACSL
- Daikon
- Caduceus
- JML
- Frama-C
- Omnibus
- Why3
- Alt-Ergo
- cvc3
- Gappa
- ISP
- Spec#
- SIMPLIFY
- TASS_
This page was built for software: KRAKATOA
