swMATH2126MaRDI QIDQ14670FDOQ14670
Author name not available (Why is that?)
Official website: http://www.cs.utah.edu/~sjt/seminar/larch/
Cited In (only showing first 100 items - show all)
- Snapshot Generation in a Constructive Object-Oriented Modeling Language
- Modular correctness proofs of behavioural implementations
- A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
- Class invariants as abstract interpretation of trace semantics
- Modular Specification of Encapsulated Object-Oriented Components
- Essential concepts of algebraic specification and program development
- Title not available (Why is that?)
- Term rewriting and beyond -- theorem proving in Isabelle
- Exploring abstract algebra in constructive type theory
- Theories for mechanical proofs of imperative programs
- Order-sorted algebraic specifications with higher-order functions
- Title not available (Why is that?)
- SOS formats and meta-theory: 20 years after
- Generate \& check method for verifying transition systems in CafeOBJ
- Title not available (Why is that?)
- Program derivation with verified transformations — a case study
- Constraining interference in an object-based design method
- Foundations of algebraic specification and formal software development.
- Title not available (Why is that?)
- Title not available (Why is that?)
- Domain modeling-based software engineering. A formal approach
- Observational interpretation of Casl specifications
- Modeling and verification of real-time systems based on equations
- How the design of JML accommodates both runtime assertion checking and formal verification
- Behavioral interface specification languages
- Behavioural theories and the proof of behavioural properties
- Combining matching algorithms: The regular case
- Title not available (Why is that?)
- Title not available (Why is that?)
- Modular specification and verification of object-oriented programs
- A logical analysis of aliasing in imperative higher-order functions
- HasCasl
- Title not available (Why is that?)
- CASL
- JML
- LETOS
- OBJ3
- CafeOBJ
- 2OBJ
- JUnit
- NQTHM
- Constructor-based observational logic
- Codecharts
- HighSpec
- SbReve2
- LOOP
- CoCasl
- UNITY
- PolyTOIL
- Reasoning with conditional axioms
- Splint
- CafeInMaude
- Houdini
- MiniMaple
- mural
- CITP
- ABCL
- AFFIRM
- REVE
- RRL
- TAME
- Tecton
- Secondary Sylow
- Jass
- CiMPA
- CiMPG
- Amulet
- ANNA
- qGCL
- Object-oriented specification and open distributed systems
- Proof systems for structured specifications with observability operators
- Verifying atomic data types
- Some experiments with a completion theorem prover
- HasCasl: integrated higher-order specification and program development
- Title not available (Why is that?)
- An overview of LP, the Larch Prover
- Specification and verification challenges for sequential object-oriented programs
- Title not available (Why is that?)
- Modular invariants for layered object structures
- An overview of the Tecton proof system
- Modular higher-order E-unification
- The definition of Extended ML: A gentle introduction
- Relating CASL with other specification languages: the institution level.
- Termination of rewrite systems by elementary interpretations
- A formal proof generator from semi-formal proof documents
- Modular specification of frame properties in JML
- Partial functions and logics: A warning
- The meaning of specifications I: Domains and initial models
- An assertional proof of red-black trees using Dafny
- Executing formal specifications with concurrent constraint programming
- A preliminary software engineering theory as investigated by published experiments
- Title not available (Why is that?)
- FORMAL VALIDATION AND VERIFICATION OF ATOMIC RESOLUTION MICROSCOPE CONTROL AND TOPOGRAPHY
- Rewrite systems for integer arithmetic
- Title not available (Why is that?)
- A formal notation and tool for the engineering of CORBA systems
- VerX
- Equality in computer algebra and beyond.
- Omitting types theorem in hybrid dynamic first-order logic with rigid symbols
- Towards the formal specification and verification of Maple programs
This page was built for software: LARCH
