LARCH

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