CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Generating counterexamples for structural inductions by exploiting nonstandard models

J.C. Blanchette ; Koen Claessen (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Lecture Notes in Computer Science. 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-17, Yogyakarta, 10-15 October 2010 (0302-9743). Vol. 6397 (2010), p. 127-141.
[Konferensbidrag, refereegranskat]

Induction proofs often fail because the stated theorem is noninductive, in which case the user must strengthen the theorem or prove auxiliary properties before performing the induction step. (Counter)model finders are useful for detecting non-theorems, but they will not find any counterexamples for noninductive theorems. We explain how to apply a well-known concept from first-order logic, nonstandard models, to the detection of noninductive invariants. Our work was done in the context of the proof assistant Isabelle/HOL and the counterexample generator Nitpick.

Denna post skapades 2012-02-10.
CPL Pubid: 155002


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers) (2008-2010)


Information Technology

Chalmers infrastruktur