Mechanised support for sound refinement tactics

No abstract is available for this paper.

• Publication year

  2011

• Venue

  Formal Aspects of Computing

• Publication date

  Unknown publication date

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1007/s00165-011-0218-z
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Unifying Theories of Programming

  2012cited by this paper
• Formal Methods for Components and Objects

  2012cited by this paper
• A tactic language for refinement of state-rich concurrent specifications

  2011cited by this paper
• Automating Refinement of Circus Programs

  2010cited by this paper
• Communication Systems in ClawZ

  2010cited by this paper
• Supporting ArcAngel in ProofPower

  2009cited by this paper
• Mechanical reasoning about families of UTP theories

  2009cited by this paper
• A UTP semantics for Circus

  2009cited by this paper
• Patterns for Refinement Automation

  2009cited by this paper
• Encoding Circus Programs in ProofPowerZ

  2008cited by this paper
• ArcAngelC: a Refinement Tactic Language for Circus

  2008cited by this paper
• Relational selves as self-affirmational resources

  2008cited by this paper
• Angelic nondeterminism in the unifying theories of programming

  2006cited by this paper
• Verification of control systems using Circus

  2006cited by this paper
• CLawZ: cost-effective formal verification for control systems

  2005cited by this paper
• Using the Compliance Notation in Industry

  2004cited by this paper
• Refine and gabriel: support for refinement and tactics

  2004cited by this paper
• ArcAngel: a Tactic Language for Refinement

  2003cited by this paper
• Refinement and the Z schema calculus

  2002cited by this paper
• ClawZ: control laws in Z

  2000cited by this paper
• ZRC – A Refinement Calculus for Z

  1998cited by this paper
• A Program Refinement Tool

  1998cited by this paper
• The Refinement Calculator: Proof Support for Program Refinement

  1997cited by this paper
• Improving Angel's Parallel Operator: Gumtree's Approach

  1997cited by this paper
• A Tactic Language for Ergo

  1997cited by this paper
• The Theory and Practice of Concurrency

  1997cited by this paper
• ML for the Working Programmer (2nd edition) by L. C. Paulson, Cambridge University Press, 1996. A Practical Course in Functional Programming Using Standard ML by R. Bosworth, McGraw Hill, 1996.

  1997cited by this paper
• The B-book - assigning programs to meanings

  1996cited by this paper
• A tactic calculus — abridged version

  1996cited by this paper
• ML for the working programmer (2. ed.)

  1996cited by this paper
• Using Z - specification, refinement, and proof

  1996cited by this paper
• Infinite Lists for Specifying Functional Programs in Z

  1996cited by this paper
• Machine-assisted theorem-proving for software engineering

  1994cited by this paper
• A language of refinements

  1994cited by this paper
• Program Refinement by Theorem Prover

  1994cited by this paper
• A Review of Existing Refinement Tools

  1994cited by this paper
• A Window Inference Tool for Refinement

  1992cited by this paper
• A Tactic Driven Refinement Tool

  1992cited by this paper
• Programming from specifications

  1990cited by this paper
• Definition of standard ML

  1990cited by this paper
• An Overview of a Refinement Editor

  1990cited by this paper
• Tool Support for the Refinement Calculus

  1990cited by this paper
• Tool Support for the Refinement Calculus.

  1990cited by this paper
• The specification statement

  1988cited by this paper
• A Discipline of Programming

  1976cited by this paper
• On the calculus of relations

  1941cited by this paper
• Under Consideration for Publication in Formal Aspects of Computing Unifying Theories in Proofpower-z

  year unknowncited by this paper

• Safelet Setup Mission Initialisation Mission Cleanup Safelet Termination Execute next Mission Event Handlers

  2016cites this paper
• Laws of mission-based programming

  2015cites this paper
• Refinement-based verification of implementations of Stateflow charts

  2014cites this paper
• Combining CSP and Object-Z

  2014cites this paper
• Grant Agreement: 287829 Comprehensive Modelling for Advanced Systems of Systems

  2014cites this paper
• Safety-critical Java programs from Circus models

  2013cites this paper
• Refining SCJ Mission Specifications into Parallel Handler Designs

  2013cites this paper