Spec#

swMATH4598MaRDI QIDQ16769FDOQ16769

Author name not available (Why is that?)

Cited In (only showing first 100 items - show all)

• Verifying Heap-Manipulating Programs in an SMT Framework
• A Realizability Model for Impredicative Hoare Type Theory
• Verifying Reference Counting Implementations
• LMS-Verify: abstraction without regret for verified systems programming
• Using History Invariants to Verify Observers
• Formal verification of a Java component using the RESOLVE framework
• Programming Languages and Systems
• Faster and more complete extended static checking for the Java modeling language
• HOL-Boogie -- an interactive prover-backend for the verifying C compiler
• Sequential, Parallel, and Quantified Updates of First-Order Structures
• Zeno: An Automated Prover for Properties of Recursive Data Structures
• Dafny: An Automatic Program Verifier for Functional Correctness
• CVPP: A Tool Set for Compositional Verification of Control–Flow Safety Properties
• Automata-based verification of programs with tree updates
• Beyond contracts for concurrency
• Contracts for concurrency
• Contract-based verification of MATLAB-style matrix programs
• Automatic verification of Java programs with dynamic frames
• Modular Safety Checking for Fine-Grained Concurrency
• Abstract Interpretation of Symbolic Execution with Explicit State Updates
• Towards imperative modules: reasoning about invariants and sharing of mutable state
• Verification conditions are code
• On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
• HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• On deciding satisfiability by theorem proving with speculative inferences
• Assertion-based slicing and slice graphs
• Refinement and verification in component-based model-driven design
• Local Reasoning for Global Invariants, Part II
• Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development
• Using First-Order Theorem Provers in the Jahob Data Structure Verification System
• A Representation-Independent Behavioral Semantics for Object-Oriented Components
• Towards the Formal Specification and Verification of Maple Programs
• Lazy behavioral subtyping
• Observational purity and encapsulation
• Modular inference of subprogram contracts for safety checking
• Behavioral interface specification languages
• A shape graph logic and a shape system
• Viper: A Verification Infrastructure for Permission-Based Reasoning
• Multi-Prover Verification of Floating-Point Programs
• Play to Test
• A sound and complete reasoning system for asynchronous communication with shared futures
• Ynot
• Verification of Concurrent Systems with VerCors
• Understanding parameters of deductive verification: an empirical investigation of KeY
• A parametric segmentation functor for fully automatic and scalable array content analysis
• Valigator: A Verification Tool with Bound and Invariant Generation
• Unifying separation logic and region logic to allow interoperability
• Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes
• Verification of Higher-Order Computation: A Game-Semantic Approach
• Stepwise refinement of heap-manipulating code in Chalice
• Invariant based programming: Basic approach and teaching experiences
• Doomed program points
• A Rewriting Logic Semantics Approach to Modular Program Analysis
• Programming Languages and Systems
• Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
• An extensible encoding of object-oriented data models in HOL. With an application to IMP++
• Modular verification of programs with effects and effects handlers
• An Algebraic Semantics for Contract-Based Software Components
• A generic framework for symbolic execution: a coinductive approach
• Specification and verification challenges for sequential object-oriented programs
• Fundamentals of software engineering. 6th international conference, FSEN 2015, Tehran, Iran, April 22--24, 2015. Revised selected papers
• Theory and methodology of assumption/commitment based system interface specification and architectural contracts
• Programming Languages and Systems
• E-matching for fun and profit
• A proof outline logic for object-oriented programming
• Effective interactive proofs for higher-order imperative programs
• Fundamental Approaches to Software Engineering
• On assertion-based encapsulation for object invariants and simulations
• Modular reasoning about heap paths via effectively propositional formulas
• Abstract Predicates and Mutable ADTs in Hoare Type Theory
• Formal verification of numerical programs: from C annotated programs to mechanical proofs
• Back to the future
• Hoare type theory, polymorphism and separation
• Synthesizing precise and useful commutativity conditions
• Second-Order Programs with Preconditions
• Verifying Whiley programs with Boogie
• ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
• Formal verification of side-channel countermeasures using self-composition
• Interleaving Symbolic Execution and Partial Evaluation
• A Refinement Methodology for Object-Oriented Programs
• Invariants Synthesis over a Combined Domain for Automated Program Verification
• ExplainHoudini: Making Houdini Inference Transparent
• An extended account of contract monitoring strategies as patterns of communication
• Verification by Parallelization of Parametric Code
• Synthesis of positive logic programs for checking a class of definitions with infinite quantification
• WP Semantics and Behavioral Subtyping
• Zap: Automated Theorem Proving for Software Analysis
• Hardware-Dependent Proofs of Numerical Programs
• Access permission contracts for scripting languages
• Are the logical foundations of verifying compiler prototypes matching user expectations?
• Title not available (Why is that?)
• RustHorn: CHC-Based Verification for Rust Programs
• Traits: correctness-by-construction for free
• Model-Based Mutation Testing of Reactive Systems
• An Assertional Proof of the Stability and Correctness of Natural Mergesort
• Holistic Specifications for Robust Programs
• Skill-Based Verification of Cyber-Physical Systems
• Exploiting pointer analysis in memory models for deductive verification
• Proving Correctness and Security of Two-Party Computation Implemented in Java in Presence of a Semi-honest Sender

This page was built for software: Spec#