Spec#
From MaRDI portal
Spec
Cited in
(only showing first 100 items - show all)- Refinement and verification in component-based model-driven design
- Invariant based programming: Basic approach and teaching experiences
- An extensible encoding of object-oriented data models in HOL. With an application to IMP++
- CVPP
- Dafny
- HOL-Boogie
- JDD
- BDD
- Valigator
- IMP++
- jContractor
- Ada95
- ArcAngel
- LARCH
- SCOOP
- TASC
- HOL-Z
- SPARK
- KRAKATOA
- Eiffel
- ACSL
- Theory and methodology of assumption/commitment based system interface specification and architectural contracts
- Why3
- JML
- Omnibus
- distcc
- Caduceus
- Frama-C
- cvc3
- Alt-Ergo
- SIMPLIFY
- OptiML
- Rascal
- Understanding parameters of deductive verification: an empirical investigation of KeY
- Unifying separation logic and region logic to allow interoperability
- Zap
- Rodin
- ESC/Java
- VCC
- JUnit
- Pex
- Assertion-based slicing and slice graphs
- Stepwise refinement of heap-manipulating code in Chalice
- Formal verification of numerical programs: from C annotated programs to mechanical proofs
- MAVEN
- Chalice
- VeriFast
- Boogie
- JACK
- Modular verification of programs with effects and effects handlers
- Verifying Whiley programs with Boogie
- Leon
- Traits: correctness-by-construction for free
- Cyclone
- WhyML
- VeriCool
- HighSpec
- Smallfoot
- TVLA
- Coquet
- Amphion
- KeY
- KIV
- FixBag
- Synthesizing precise and useful commutativity conditions
- LOOP
- Exploiting pointer analysis in memory models for deductive verification
- VerCors
- jStar
- SpecExplorer
- Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
- Ynot
- Jahob
- Formal verification of side-channel countermeasures using self-composition
- CSPsim
- Contract
- SmallEiffel
- Grasshopper
- A proof outline logic for object-oriented programming
- BVD
- Clara
- Synthesis of positive logic programs for checking a class of definitions with infinite quantification
- Are the logical foundations of verifying compiler prototypes matching user expectations?
- On assertion-based encapsulation for object invariants and simulations
- Specification and verification challenges for sequential object-oriented programs
- Faster and more complete extended static checking for the Java modeling language
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- Viper
- THOR
- Viper: a verification infrastructure for permission-based reasoning
- Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
- Featherweight Java
- Contract-based verification of MATLAB-style matrix programs
- EventB2Dafny
- Model-Based Mutation Testing of Reactive Systems
- Invariants synthesis over a combined domain for automated program verification
- E-matching for fun and profit
- From predicates to programs: the semantics of a method language
- Behavioral interface specification languages
- Zeno: an automated prover for properties of recursive data structures
This page was built for software: Spec#
