@inproceedings{10.1007/978-3-540-24730-2_2,
    Abstract = {We present a method of deriving Craig interpolants from proofs in the quantifier-free theory of linear inequality and uninterpreted function symbols, and an interpolating theorem prover based on this method. The prover has been used for predicate refinement in the Blast software model checker, and can also be used directly for model checking infinite-state systems, using interpolation-based image approximation.},
    Address = {Berlin, Heidelberg},
    Author = {McMillan, K. L.},
    BookTitle = {Tools and Algorithms for the Construction and Analysis of Systems},
    Editor = {Jensen, Kurt and Podelski, Andreas},
    File = {An Interpolating Theorem Prover - McMillan2004\_Chapter\_AnInterpolatingTheoremProver (0) - a - a - b.pdf},
    ISBN = {978-3-540-24730-2},
    Pages = {16--30},
    Publisher = {Springer Berlin Heidelberg},
    Title = {An Interpolating Theorem Prover},
    Year = {2004},
    date-added = {2019-10-09 21:57:51 +0200},
    date-modified = {2019-10-09 21:57:51 +0200},
    doi = {10.1007/978-3-540-24730-2_2}
}

@inproceedings{10.1007/978-3-540-24730-2_2, Abstract = {We present a method of deriving Craig interpolants from proofs in the quantifier-free theory of linear inequality and uninterpreted function symbols, and an interpolating theorem prover based on this method. The prover has been used for predicate refinement in the Blast software model checker, and can also be used directly for model checking infinite-state systems, using interpolation-based image approximation.}, Address = {Berlin, Heidelberg}, Author = {McMillan, K. L.}, BookTitle = {Tools and Algorithms for the Construction and Analysis of Systems}, Editor = {Jensen, Kurt and Podelski, Andreas}, File = {An Interpolating Theorem Prover - McMillan2004_Chapter_AnInterpolatingTheoremProver (0) - a - a - b.pdf}, ISBN = {978-3-540-24730-2}, Pages = {16--30}, Publisher = {Springer Berlin Heidelberg}, Title = {An Interpolating Theorem Prover}, Year = {2004}, date-added = {2019-10-09 21:57:51 +0200}, date-modified = {2019-10-09 21:57:51 +0200}, doi = {10.1007/978-3-540-24730-2_2} }