Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014

No abstract is available for this paper.

• Publication year

  2016

• Venue

  Leveraging Applications of Formal Methods

• Publication date

  2016-10-10

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1007/978-3-319-47166-2_32
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Abstract Software Specifications and Automatic Proof of Refinement

  2016cited by this paper
• Counterexamples from Proof Failures in SPARK

  2016cited by this paper
• Integrated Environment for Diagnosing Verification Errors

  2016cited by this paper
• Frama-C: A software analysis perspective

  2015influential reference
• Your Proof Fails? Testing Helps to Find the Reason

  2015cited by this paper
• Software Architecture of Code Analysis Frameworks Matters: The Frama-C Example

  2015cited by this paper
• Rester statique pour devenir plus rapide, plus précis et plus mince

  2015cited by this paper
• AutoProof: auto-active functional verification of object-oriented programs

  2015cited by this paper
• Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK

  2014cited by this paper
• The spirit of ghost code

  2014cited by this paper
• The Dafny Integrated Development Environment

  2014influential reference
• OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse

  2014cited by this paper
• Formalizing Semantics with an Automatic Program Verifier

  2014cited by this paper
• B Extended to Floating‐Point Numbers: Is it Sufficient for Proving Avionics Software?

  2014cited by this paper
• Automatically Verified Implementation of Data Structures Based on AVL Trees

  2014cited by this paper
• Explicit Assumptions - A Prenup for Marrying Static and Dynamic Program Verification

  2014cited by this paper
• Verified programs with binders

  2014cited by this paper
• Runtime Assertion Checking and Its Combinations with Static and Dynamic Analyses - Tutorial Synopsis

  2014cited by this paper
• Synthesis modulo recursive functions

  2013cited by this paper
• Common specification language for static and dynamic analysis of C programs

  2013cited by this paper
• Program Checking with Less Hassle

  2013cited by this paper
• A Lesson on Runtime Assertion Checking with Frama-C

  2013influential reference
• Why3 - Where Programs Meet Provers

  2013cited by this paper
• An Optimized Memory Monitoring for Runtime Assertion Checking of C Programs

  2013cited by this paper
• Automating Induction with an SMT Solver

  2012cited by this paper
• δ-Complete Decision Procedures for Satisfiability over the Reals

  2012cited by this paper
• Combining Analyses for C Program Verification

  2012cited by this paper
• The New Quickcheck for Isabelle - Random, Exhaustive and Symbolic Testing under One Roof

  2012cited by this paper
• Correct Code Containing Containers

  2011cited by this paper
• ACSL: ANSI/ISO C Specification Language

  2008influential reference
• The Why/Krakatoa/Caduceus Platform for Deductive Program Verification

  2007cited by this paper
• Reassessing JML’s Logical Foundation

  2005cited by this paper
• Logical foundations of program assertions: what do practitioners want?

  2005cited by this paper
• Multi-prover Verification of C Programs

  2004cited by this paper
• The KRAKATOA tool for certificationof JAVA/JAVACARD programs annotated in JML

  2004cited by this paper
• The Spec# Programming System: An Overview

  2004cited by this paper
• Formal Verification of a Commercial Smart Card Applet with Multiple Tools

  2004cited by this paper
• An overview of JML tools and applications

  2003cited by this paper
• How the Design of JML Accomodates Both Runtime Assertion Checking and Formal Verification

  2002cited by this paper
• Programming in ADA

  1989cited by this paper
• 物件導向軟體之架構(Object-Oriented Software Construction)探討

  1989cited by this paper
• Verified Programs with Binders ∗

  year unknowncited by this paper

• Design of Safe C Language for Program Verification

  2026cites this paper
• Fulminate: Testing CN Separation-Logic Specifications in C

  2025cites this paper
• Static and Dynamic Verification of OCaml Programs: The Gospel Ecosystem (Extended Version)

  2024cites this paper
• Automated formal analysis of temporal properties of Ladder programs

  2022cites this paper
• Towards random and enumerative testing for OCaml and WhyML properties

  2022cites this paper
• The e-ACSL perspective on runtime assertion checking

  2021cites this paper
• Explaining Counterexamples with Giant-Step Assertion Checking

  2021cites this paper
• Giant-step Semantics for the Categorisation of Counterexamples

  2021cites this paper
• Efficient Runtime Assertion Checking for Properties over Mathematical Numbers

  2020cites this paper
• Rapport d'avancement sur la vérification formelle des algorithmes de ParcourSup

  2020cites this paper
• Fast and Effective Well-Definedness Checking

  2020cites this paper
• Unit Lemmas for Detecting Requirement and Specification Flaws

  2020cites this paper
• Towards a Formally Verified Space Mission Software using SPARK

  2019cites this paper
• D 1 . 5 Analyses choice methodology report

  2019cites this paper
• GOSPEL - Providing OCaml with a Formal Specification Language

  2019cites this paper
• Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools

  2019cites this paper
• Proof Strategy for Automated Sisal Program Verification

  2019cites this paper
• Program Verification in the Presence of I/O - Semantics, Verified Library Routines, and Verified Applications

  2018cites this paper
• Instrumenting a weakest precondition calculus for counterexample generation

  2018cites this paper
• Safe and Secure Autopilot Software for Drones

  2018cites this paper
• Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software

  2018cites this paper
• Auto-Active Proof of Red-Black Trees in SPARK

  2017cites this paper
• L'Assistant de Preuve Coq Table des matières

  2017cites this paper
• Automating the Verification of Floating-Point Programs

  2017cites this paper
• How to Get an Efficient yet Verified Arbitrary-Precision Integer Library

  2017cites this paper
• Predicting SMT Solver Performance for Software Verification

  2017cites this paper
• Verified Software. Theories, Tools, and Experiments

  2017cites this paper
• Static and Runtime Verification, Competitors or Friends? (Track Summary)

  2016cites this paper
• Automating the Verification of Floating-Point Programs (cid:63)

  year unknowncites this paper
• Generating and Certifying Accuracy Properties of Floating-Point Programs

  year unknowncites this paper
• Conformity of Ladder Programs against State Transition Diagrams

  year unknowncites this paper
• Formal Analysis of Ladder Programs using Deductive Verification

  year unknowncites this paper