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

Automating Inductive Proofs using Theory Exploration

Koen Claessen (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Dan Rosén (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Moa Johansson (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Nicholas Smallbone (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013 (0302-9743). Vol. 7898 (2013), p. 392-406.
[Konferensbidrag, refereegranskat]

HipSpec is a system for automatically deriving and proving properties about functional programs. It uses a novel approach, combining theory exploration, counterexample testing and inductive theorem proving. HipSpec automatically generates a set of equational theorems about the available recursive functions of a program. These equational properties make up an algebraic specification for the program and can in addition be used as a background theory for proving additional user-stated properties. Experimental results are encouraging: HipSpec compares favourably to other inductive theorem provers and theory exploration systems.

Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2013-04-08. Senast ändrad 2015-12-17.
CPL Pubid: 175485


Läs direkt!

Lokal fulltext (fritt tillgänglig)

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