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

A Parametric Interpolation Framework for First-Order Theories

Laura Kovacs (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Natasha Sharygina ; Simone Fulvio Rollini
Proceedings of the 12th Mexican International Conference on Artificial Intelligence - Advances in Artificial Intelligence and Its Applications (MICAI 2013), November 24-30, 2013, Mexico City, Mexico. Felix Castro and Alexander F. Gelbukh and Miguel Gonzalez (editors), Springer Lectures Notes in Computer Science Vol. LNCS 8265 (2013), p. 24-40.
[Konferensbidrag, refereegranskat]

Craig interpolation is successfully used in both hardware and software model checking. Generating good interpolants, and hence automatic understanding of the quality of interpolants is however a very hard problem, requiring non-trivial reasoning in first-order theories. An important class of state-of-the-art interpolation algorithms is based on recursive procedures that generate interpolants from refutations of unsatisfiable conjunctions of formulas. We analyze this type of algorithms and develop a theoretical framework, called a parametric interpolation framework, for arbitrary first-order theories and inference systems. As interpolation-based verification approaches depend on the quality of interpolants, our method can be used to derive interpolants of different structure and strength, with or without quantifiers, from the same proof. We show that some well-known interpolation algorithms are instantiations of our framework.

Nyckelord: program verification, formal methods, interpolation, first-order logic, theorem proving



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: 191602

 

Läs direkt!


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