KeY
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Refinement and retrenchment for programming language data types
- Automatic Validation of Transformation Rules for Java Verification Against a Rewriting Semantics
- Second-Order Principles in Specification Languages for Object-Oriented Programs
- Verifying OpenJDK's sort method for generic collections
- Verifying Whiley programs with Boogie
- CRADLE
- White-Box Testing by Combining Deduction-Based Specification Extraction and Black-Box Testing
- Automating Verification of Loops by Parallelization
- Sequential, Parallel, and Quantified Updates of First-Order Structures
- A logic for secure memory access of abstract state machines
- Proof pearl: The KeY to correct and stable sorting
- Automated Deduction – CADE-20
- Deductive verification of floating-point Java programs in KeY
- Principled software development. Essays dedicated to Arnd Poetzsch-Heffter on the occasion of his 60th birthday. Selected papers based on the presentations at the symposium, Kaiserslautern, Germany, November 2018
- KeYmaera X: an axiomatic tactical theorem prover for hybrid systems
- Simplify: a theorem prover for program checking
- Fundamental Approaches to Software Engineering
- A universal machine for biform theory graphs
- Assertion-based slicing and slice graphs
- A program logic for resources
- Integrated Formal Methods
- Ensuring the correctness of lightweight tactics for JavaCard dynamic logic
- Are the logical foundations of verifying compiler prototypes matching user expectations?
- Abstract State Machines 2004. Advances in Theory and Practice
- Mechanical inference of invariants for FOR-loops
- Invariant-driven specifications in Maude
- Gray-box monitoring of hyperproperties with an application to privacy
- Logical Aspects of Computational Linguistics
- Aligator
- Dafny
- JMLUnit
- KeY-C
- Alloy
- IMP++
- Symstra
- SecureUML
- LARCH
- ADORA
- HOL-Z
- KRAKATOA
- SPARK
- Eiffel
- KeYmaera
- ACSL
- Caduceus
- JML
- Frama-C
- Why3
- Alt-Ergo
- Spec#
- KLEE
- HOL-OCL
- ESC/Java
- Eclat
- Scala
- JUnit
- Rostra
- Z2sal
- JACK
- Boogie
- VeriFast
- Alcoa
- TRX
- Multilisp
- Aligators
- SOCLE
- Athena
- ATL
- JKelloy
- Kelloy
- vUML
- FixBag
- KIV
- DiaGen
- WhyML
- LOOP
- UML2Alloy
- ArgoUML
- Viper
- Zen
- VerCors
- UMLtoCSP
- GF
- Lingva
- BVD
- Snugglebug
- DynaMate
- VCGen
- THOR
- Grail
- Jaza
- Java Jr
- Splint
- Averist
- OpenJML
- Quicksort
- ABS
- Stabhyli
- CertiKOS
- LARVA
This page was built for software: KeY
