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

First-Order Theorem Proving and Vampire

Laura Kovacs (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Andrei Voronkov
Proceedings of the 25th International Conference on Computer Aided Verification (CAV 2013), July 13-19, 2013, Saint Petersburg, Russia, Natasha Sharygina and Helmut Veith (editors), Springer Lecture Notes in Computer Sciences Vol. LNCS 8044 (2013), p. 1-35.
[Konferensbidrag, refereegranskat]

In this paper we give a short introduction in first-order theorem proving and the use of the theorem prover VAMPIRE. We discuss the superposition calculus and explain the key concepts of saturation and redundancy elimination, present saturation algorithms and preprocessing, and demonstrate how these concepts are implemented in VAMPIRE. Further, we also cover more recent topics and features of VAMPIRE designed for advanced applications, including satisfiability checking, theory reasoning, interpolation, consequence elimination, and program analysis.

Nyckelord: formal methods, theorem proving, automated reasoning, program analysis, program verification, software engineering



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

Läs mer om Chalmers styrkeområden  

Denna post skapades 2014-01-07. Senast ändrad 2016-08-22.
CPL Pubid: 191553

 

Läs direkt!


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