The following pages link to LARCH (Q14670):
Displaying 50 items.
- Foundations of algebraic specification and formal software development. (Q610397) (← links)
- Behavioural theories and the proof of behavioural properties (Q671500) (← links)
- The meaning of specifications I: Domains and initial models (Q673181) (← links)
- Partial functions and logics: A warning (Q673461) (← links)
- SOS formats and meta-theory: 20 years after (Q877025) (← links)
- Modeling and verification of real-time systems based on equations (Q882458) (← links)
- Term rewriting and beyond -- theorem proving in Isabelle (Q909488) (← links)
- Verifying atomic data types (Q914403) (← links)
- HasCasl: integrated higher-order specification and program development (Q1006648) (← links)
- Modular correctness proofs of behavioural implementations (Q1127821) (← links)
- Some experiments with a completion theorem prover (Q1186705) (← links)
- Combining matching algorithms: The regular case (Q1186723) (← links)
- A semi-algorithm for algebraic implementation proofs (Q1199928) (← links)
- Theories for mechanical proofs of imperative programs (Q1267030) (← links)
- Gordon's computer: A hardware verification case study in OBJ3 (Q1329091) (← links)
- An overview of the Tecton proof system (Q1341710) (← links)
- Verifying a distributed list system: A case history (Q1355754) (← links)
- Essential concepts of algebraic specification and program development (Q1377322) (← links)
- Order-sorted algebraic specifications with higher-order functions (Q1391097) (← links)
- Proof systems for structured specifications with observability operators (Q1391730) (← links)
- The definition of Extended ML: A gentle introduction (Q1391731) (← links)
- Equality in computer algebra and beyond. (Q1404423) (← links)
- Deductive verification of real-time systems using STeP (Q1589585) (← links)
- A formal proof generator from semi-formal proof documents (Q1675786) (← links)
- Class invariants as abstract interpretation of trace semantics (Q1749225) (← links)
- How the design of JML accommodates both runtime assertion checking and formal verification (Q1776585) (← links)
- Termination of rewrite systems by elementary interpretations (Q1805401) (← links)
- Relating CASL with other specification languages: the institution level. (Q1853458) (← links)
- Executing formal specifications with concurrent constraint programming (Q1857312) (← links)
- A preliminary software engineering theory as investigated by published experiments (Q1859416) (← links)
- Models and tools for managing development processes. (Q1878978) (← links)
- Manipulating algebraic specifications with term-based and graph-based representations (Q1885933) (← links)
- Specification and verification of object-oriented programs using supertype abstraction (Q1902305) (← links)
- Reasoning with conditional axioms (Q1924731) (← links)
- A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L (Q1961914) (← links)
- An assertional proof of red-black trees using Dafny (Q1984797) (← links)
- Semantics of multiway dataflow constraint systems (Q2043794) (← links)
- Omitting types theorem in hybrid dynamic first-order logic with rigid symbols (Q2111114) (← links)
- Modeling and visualizing object-oriented programs with Codecharts (Q2248065) (← links)
- Impact of performance considerations on formal specification design (Q2365398) (← links)
- Constructor-based observational logic (Q2369030) (← links)
- Modular invariants for layered object structures (Q2507783) (← links)
- Are the logical foundations of verifying compiler prototypes matching user expectations? (Q2643125) (← links)
- Specification and verification challenges for sequential object-oriented programs (Q2643131) (← links)
- Parameterized theories and views in full Maude 2. 0 (Q2703707) (← links)
- (Q2729071) (← links)
- Domain modeling-based software engineering. A formal approach (Q2736173) (← links)
- A system for predictable component-based software construction (Q2751752) (← links)
- (Q2763972) (← links)
- (Q2764130) (← links)
