Specification and verification

No abstract is available for this paper.

• Publication year

  2011

• Venue

  Communications of the ACM

• Publication date

  2011-06-01

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/1953122.1953145
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• No references are available for this paper.

• Interactive Abstract Interpretation with Demanded Summarization

  2024cites this paper
• Fuzzing Processing Pipelines for Zero-Knowledge Circuits

  2024cites this paper
• Co-Developing Programs and Their Proof of Correctness

  2024cites this paper
• Formalizing an Efficient Runtime Assertion Checker for an Arithmetic Language with Functions and Predicates

  2023cites this paper
• Design by Contract for Deep Learning APIs

  2023cites this paper
• Sound Runtime Assertion Checking for Memory Properties via Program Transformation

  2023cites this paper
• Modal Abstractions for Virtualizing Memory Addresses

  2023cites this paper
• Verification-Preserving Inlining in Automatic Separation Logic Verifiers

  2022cites this paper
• Language Design Meets Verifying Compilers (Keynote)

  2022cites this paper
• Bounded Model Checking of PLC ST Programs using Rewriting Modulo SMT

  2022cites this paper
• Using capabilities for strict runtime invariant checking

  2022cites this paper
• Verifying Whiley Programs with Boogie

  2022cites this paper
• Identifying Overly Restrictive Matching Patterns in SMT-based Program Verifiers (Extended Version)

  2021cites this paper
• The First Fifteen Years of the Verified Software Project

  2021cites this paper
• Formal Verification of a Java Component Using the RESOLVE Framework

  2021cites this paper
• Formally Validating a Practical Verification Condition Generator (extended version)

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

  2021cites this paper
• Verifying verified code

  2021cites this paper
• Leveraging Control Flow Knowledge in SMT Solving of Program Verification

  2021cites this paper
• Putting the semantics into semantic versioning

  2020influential citation
• FreeSpec: specifying, verifying, and executing impure computations in Coq

  2020cites this paper
• ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs

  2020cites this paper
• RustHorn: CHC-Based Verification for Rust Programs

  2020cites this paper
• Skill-Based Verification of Cyber-Physical Systems

  2020cites this paper
• Verified Runtime Assertion Checking for Memory Properties

  2020cites this paper
• Statically Checking REST API Consumers

  2020cites this paper
• Unifying execution of imperative generators and declarative specifications

  2020cites this paper
• Human-cyber-physical systems: concepts, challenges, and research opportunities

  2020cites this paper
• Modular verification of programs with effects and effects handlers

  2020cites this paper
• Towards Full Proof Automation in Frama-C Using Auto-active Verification

  2019cites this paper
• Leveraging rust types for modular specification and verification

  2019cites this paper
• Tool Support for Correctness-by-Construction

  2019cites this paper
• Feature-Oriented Contract Composition

  2019cites this paper
• Comparing Correctness-by-Construction with Post-Hoc Verification - A Qualitative User Study

  2019cites this paper
• An Introduction to Software Verification with Whiley

  2018cites this paper
• Towards compilation of an imperative language for FPGAs

  2018cites this paper
• Experience Report on Formally Verifying Parts of OpenJDK's API with KeY

  2018influential citation
• Modeling safety culture as a socially emergent phenomenon: a case study in aircraft maintenance

  2016cites this paper
• Automatic verification of Dafny programs with traits

  2015cites this paper
• iConference 2014 Proceedings

  2014cites this paper
• A Logical Analysis of Framing for Specifications with Pure Method Calls

  2014cites this paper
• Thinking About Context: Design Practices for Information Architecture with Context-Aware Systems

  2014cites this paper
• History of Interactive Theorem Proving

  2014cites this paper
• Verification of Agent-Based Artifact Systems

  2013cites this paper
• Computer-Assisted Program Reasoning Based on a Relational Semantics of Programs

  2012cites this paper
• Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control

  2012cites this paper
• Developing verified programs with Dafny

  2012cites this paper
• Getting Started with Dafny: A Guide

  2012cites this paper
• A Model-Based Ambient Agent Providing Support in Handling Desire and Temptation

  2010cites this paper
• To Goto Where No Statement Has Gone Before

  2010cites this paper
• Computer Assisted Reasoning

  2009influential citation