LARCH

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