Spec#
From MaRDI portal
Spec
Cited in
(only showing first 100 items - show all)- An assertional proof of the stability and correctness of Natural Mergesort
- Synthesizing precise and useful commutativity conditions
- Verifying Heap-Manipulating Programs in an SMT Framework
- A rewriting logic semantics approach to modular program analysis
- Verifying Reference Counting Implementations
- RustHorn: CHC-based verification for Rust programs
- WP semantics and behavioral subtyping
- A Realizability Model for Impredicative Hoare Type Theory
- Verifying Whiley programs with Boogie
- Formal verification of a Java component using the RESOLVE framework
- LMS-Verify: abstraction without regret for verified systems programming
- Using History Invariants to Verify Observers
- Skill-based verification of cyber-physical systems
- Formal verification of side-channel countermeasures using self-composition
- 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
- Towards the formal specification and verification of Maple programs
- Automata-based verification of programs with tree updates
- Beyond contracts for concurrency
- Contracts for concurrency
- Sequential, Parallel, and Quantified Updates of First-Order Structures
- Contract-based verification of MATLAB-style matrix programs
- An extended account of contract monitoring strategies as patterns of communication
- 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
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- On deciding satisfiability by theorem proving with speculative inferences
- Viper: a verification infrastructure for permission-based reasoning
- Synthesis of positive logic programs for checking a class of definitions with infinite quantification
- Verification by Parallelization of Parametric Code
- Assertion-based slicing and slice graphs
- Dynamic boundaries: information hiding by second order framing with first order assertions
- Refinement and verification in component-based model-driven design
- Zap: Automated Theorem Proving for Software Analysis
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System
- A Representation-Independent Behavioral Semantics for Object-Oriented Components
- Hardware-Dependent Proofs of Numerical Programs
- Access permission contracts for scripting languages
- Are the logical foundations of verifying compiler prototypes matching user expectations?
- Lazy behavioral subtyping
- Observational purity and encapsulation
- Modular inference of subprogram contracts for safety checking
- Enforcing structural invariants using dynamic frames
- Behavioral interface specification languages
- DKAL and Z3: a logic embedding experiment
- CVPP
- Dafny
- HOL-Boogie
- Valigator
- IMP++
- jContractor
- Ada95
- ArcAngel
- LARCH
- SCOOP
- TASC
- HOL-Z
- KRAKATOA
- SPARK
- Eiffel
- ACSL
- distcc
- Caduceus
- JML
- Frama-C
- Omnibus
- Why3
- Alt-Ergo
- cvc3
- SIMPLIFY
- OptiML
- Rascal
- Zap
- Rodin
- ESC/Java
- JUnit
- Pex
- VCC
- JACK
- Boogie
- Chalice
- MAVEN
- VeriFast
- Leon
- Cyclone
- HighSpec
- Amphion
- Coquet
- Smallfoot
- KeY
- FixBag
- KIV
- WhyML
- VeriCool
This page was built for software: Spec#
