LARCH
From MaRDI portal
Software:14670
swMATH2126MaRDI QIDQ14670FDOQ14670
Author name not available (Why is that?)
Cited In (only showing first 100 items - show all)
- Snapshot Generation in a Constructive Object-Oriented Modeling Language
- Executing formal specifications with concurrent constraint programming
- A preliminary software engineering theory as investigated by published experiments
- 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?)
- Equality in computer algebra and beyond.
- Term rewriting and beyond -- theorem proving in Isabelle
- Exploring abstract algebra in constructive type theory
- Theories for mechanical proofs of imperative programs
- Models and tools for managing development processes.
- Order-sorted algebraic specifications with higher-order functions
- Title not available (Why is that?)
- SOS formats and meta-theory: 20 years after
- Title not available (Why is that?)
- Title not available (Why is that?)
- Program derivation with verified transformations — a case study
- Constraining interference in an object-based design method
- Rewriting, and equational unification: the higher-order cases
- Title not available (Why is that?)
- Foundations of algebraic specification and formal software development.
- Title not available (Why is that?)
- Title not available (Why is that?)
- Object-Oriented Specification and Open Distributed Systems
- Towards the Formal Specification and Verification of Maple Programs
- 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?)
- Specification and verification of object-oriented programs using supertype abstraction
- 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
- Title not available (Why is that?)
- Constructor-based observational logic
- Reasoning with conditional axioms
- Gordon's computer: A hardware verification case study in OBJ3
- Some Tips on Writing Proof Scores in the OTS/CafeOBJ Method
- 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?)
- A semi-algorithm for algebraic implementation proofs
- 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?)
- Verifying a distributed list system: A case history
- Modular invariants for layered object structures
- An overview of the Tecton proof system
- Modular higher-order E-unification
- Generate & Check Method for Verifying Transition Systems in CafeOBJ
- 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
- Deductive verification of real-time systems using STeP
- Partial functions and logics: A warning
- The meaning of specifications I: Domains and initial models
- An assertional proof of red-black trees using Dafny
- 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
- Omitting types theorem in hybrid dynamic first-order logic with rigid symbols
- Title not available (Why is that?)
- A system for predictable component-based software construction
- Title not available (Why is that?)
- Manipulating algebraic specifications with term-based and graph-based representations
- Title not available (Why is that?)
- Modeling and visualizing object-oriented programs with Codecharts
- Title not available (Why is that?)
- Title not available (Why is that?)
- Algebra and automated deduction
- Generic Proof Scores for Generate & Check Method in CafeOBJ
- Title not available (Why is that?)
- Are the logical foundations of verifying compiler prototypes matching user expectations?
- Impact of performance considerations on formal specification design
- Recent Trends in Algebraic Development Techniques
- Semantics of multiway dataflow constraint systems
- Title not available (Why is that?)
- Combining matching algorithms: The regular case
- The deductive IDEF1X data model of a tooling system
- Title not available (Why is that?)
- Program Development in Computational Logic
- Holistic Specifications for Robust Programs
- Goldilocks and the three specifications
- Specifications can make programs run faster
- Ours Is to Reason Why
This page was built for software: LARCH