An overview of the Tecton proof system. The Tecton proof system is an experimental tool for constructing proofs of first-order logic formulas and of program specifications expressed using formulas in Hoare’s axiomatic proof formalism. It is designed to make interactive proof construction easier than with previous proof tools, by maintaining multiple proof attempts internally in a structured form called a proof forest; displaying them in an easy to comprehend form, using a combination of tabular formats, graphical representations, and hypertext links; and automating substantial parts of proofs through rewriting, induction, case analysis, and generalization inference mechanisms, along with a linear arithmetic decision procedure. Further development of the system is planned as part of an overall framework aimed at supporting the kind of abstractions and specializations necessary for building libraries of generic software and hardware components.

References in zbMATH (referenced in 9 articles , 1 standard article )

Showing results 1 to 9 of 9.
Sorted by year (citations)

  1. Bourdev, Lubomir; Järvi, Jaakko: Efficient run-time dispatching in generic programming with minimal code bloat (2011) ioport
  2. Gregor, Douglas; Järvi, Jaakko; Kulkarni, Mayuresh; Lumsdaine, Andrew; Musser, David; Schupp, Sibylle: Generic programming and high-performance libraries (2005) ioport
  3. Armando, Alessandro; Ranise, Silvio: Constraint contextual rewriting. (2003)
  4. Kapur, Deepak; Subramaniam, M.: New uses of linear arithmetic in automated theorem proving by induction (1996)
  5. Simons, Martin; Weber, Matthias: An approach to literate and structured formal developments (1996)
  6. Kapur, D.; Zhang, H.: An overview of rewrite rule laboratory (RRL) (1995) ioport
  7. Kapur, D.; Nie, X.; Musser, D. R.: An overview of the Tecton proof system (1994)
  8. Kapur, D.; Nie, X.; Musser, D. R.: An overview of the tecton proof system. (1994) ioport
  9. Stavridou, Victoria: Gordon’s computer: A hardware verification case study in OBJ3 (1994)