LARCH

swMATH2126MaRDI QIDQ14670

No author found.

Related Items (only showing first 100 items - show all)

FORMAL VALIDATION AND VERIFICATION OF ATOMIC RESOLUTION MICROSCOPE CONTROL AND TOPOGRAPHY ⋮ Gordon's computer: A hardware verification case study in OBJ3 ⋮ Models and tools for managing development processes. ⋮ Holistic Specifications for Robust Programs ⋮ Impact of performance considerations on formal specification design ⋮ Unnamed Item ⋮ Goldilocks and the three specifications ⋮ Constraining interference in an object-based design method ⋮ Specifications can make programs run faster ⋮ Constructor-based observational logic ⋮ Modular specification of frame properties in JML ⋮ Manipulating algebraic specifications with term-based and graph-based representations ⋮ Unnamed Item ⋮ An overview of the Tecton proof system ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ An overview of LP, the Larch Prover ⋮ Rewriting, and equational unification: the higher-order cases ⋮ Modular higher-order E-unification ⋮ Problems in rewriting applied to categorical concepts by the example of a computational comonad ⋮ Rewrite systems for integer arithmetic ⋮ Unnamed Item ⋮ Towards the Formal Specification and Verification of Maple Programs ⋮ Verifying a distributed list system: A case history ⋮ Recent Trends in Algebraic Development Techniques ⋮ Unnamed Item ⋮ Specification and verification of object-oriented programs using supertype abstraction ⋮ Are the logical foundations of verifying compiler prototypes matching user expectations? ⋮ Specification and verification challenges for sequential object-oriented programs ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Essential concepts of algebraic specification and program development ⋮ Unnamed Item ⋮ SOS formats and meta-theory: 20 years after ⋮ A formal proof generator from semi-formal proof documents ⋮ Modular correctness proofs of behavioural implementations ⋮ Reasoning with conditional axioms ⋮ Modeling and verification of real-time systems based on equations ⋮ Foundations of algebraic specification and formal software development. ⋮ Generic Proof Scores for Generate & Check Method in CafeOBJ ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Order-sorted algebraic specifications with higher-order functions ⋮ Unnamed Item ⋮ Proof systems for structured specifications with observability operators ⋮ The definition of Extended ML: A gentle introduction ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Equality in computer algebra and beyond. ⋮ Unnamed Item ⋮ Term rewriting and beyond -- theorem proving in Isabelle ⋮ Verifying atomic data types ⋮ A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Program derivation with verified transformations — a case study ⋮ Unnamed Item ⋮ Object-Oriented Specification and Open Distributed Systems ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Some experiments with a completion theorem prover ⋮ Combining matching algorithms: The regular case ⋮ Behavioural theories and the proof of behavioural properties ⋮ The meaning of specifications I: Domains and initial models ⋮ Partial functions and logics: A warning ⋮ An assertional proof of red-black trees using Dafny ⋮ Unnamed Item ⋮ Algebra and automated deduction ⋮ Class invariants as abstract interpretation of trace semantics ⋮ Modeling and visualizing object-oriented programs with Codecharts ⋮ Unnamed Item ⋮ A semi-algorithm for algebraic implementation proofs ⋮ Unnamed Item ⋮ Modular Specification of Encapsulated Object-Oriented Components ⋮ How the design of JML accommodates both runtime assertion checking and formal verification ⋮ Combining matching algorithms: The regular case ⋮ A formal notation and tool for the engineering of CORBA systems ⋮ Modular invariants for layered object structures ⋮ Observational interpretation of Casl specifications ⋮ HasCasl: integrated higher-order specification and program development ⋮ Exploring abstract algebra in constructive type theory ⋮ Semantics of multiway dataflow constraint systems ⋮ Termination of rewrite systems by elementary interpretations ⋮ Theories for mechanical proofs of imperative programs ⋮ A logical analysis of aliasing in imperative higher-order functions ⋮ Ours Is to Reason Why ⋮ Snapshot Generation in a Constructive Object-Oriented Modeling Language ⋮ Deductive verification of real-time systems using STeP ⋮ Generate & Check Method for Verifying Transition Systems in CafeOBJ ⋮ Relating CASL with other specification languages: the institution level. ⋮ Translation Templates to Support Strategy Development in PVS ⋮ Executing formal specifications with concurrent constraint programming ⋮ A preliminary software engineering theory as investigated by published experiments ⋮ Baby Modula-3 and a theory of objects ⋮ Omitting types theorem in hybrid dynamic first-order logic with rigid symbols ⋮ Behavioral interface specification languages

This page was built for software: LARCH