×

Nitpick

swMATH ID: 622
Software Authors: Blanchette, Jasmin Christian; Nipkow, Tobias
Description: Nitpick is a counterexample generator for Isabelle/HOL that builds on Kodkod, a SAT-based first-order relational model finder. Nitpick supports unbounded quantification, (co)inductive predicates and datatypes, and (co)recursive functions. Fundamentally a finite model finder, it approximates infinite types by finite subsets. As case studies, we consider a security type system and a hotel key card system. Our experimental results on Isabelle theories and the TPTP library indicate that Nitpick generates more counterexamples than other model finders for higher-order logic, without restrictions on the form of the formulas to falsify.
Homepage: http://www4.in.tum.de/~blanchet/nitpick.html
Related Software: Isabelle/HOL; Sledgehammer; Coq; Isabelle; TPTP; PVS; HOL; LEO-II; Archive Formal Proofs; z3; Satallax; HOL Light; Kodkod; E Theorem Prover; QuickCheck; CVC4; VAMPIRE; SmallCheck; Mizar; SPASS
Cited in: 71 Publications

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
Nitpick: a counterexample generator for higher-order logic based on a relational model finder. Zbl 1291.68326
Blanchette, Jasmin Christian; Nipkow, Tobias
2010
all top 5

Cited by 104 Authors

21 Benzmüller, Christoph Ewald
11 Blanchette, Jasmin Christian
8 Guttmann, Walter
5 Paulson, Lawrence Charles
4 Fuenmayor, David
4 Reynolds, Andrew
4 Steen, Alexander
4 Woltzenlogel Paleo, Bruno
3 Nipkow, Tobias
3 Parent, Xavier
2 Abdulaziz, Mohammad
2 Berghammer, Rudolf
2 Bulwahn, Lukas
2 Bundy, Alan
2 Dubois, Catherine
2 Foster, Simon
2 Giorgetti, Alain
2 Gretton, Charles
2 Grov, Gudmund
2 Jackson, Daniel
2 Krauss, Alexander
2 Libal, Tomer
2 Lochbihler, Andreas
2 Norrish, Michael
2 Pease, Alison
2 Popescu, Andrei
2 Raggi, Daniel
2 Scott, Dana Stewart
2 Tinelli, Cesare
2 van der Torre, Leendert W. N.
2 Wenzel, Makarius
1 Avigad, Jeremy
1 Barrett, Clark W.
1 Baumgartner, Peter
1 Benda, Miroslav
1 Biendarra, Julian
1 Böhm, Peter
1 Bouzy, Aymeric
1 Cheney, James
1 Claessen, Koen
1 Cruanes, Simon
1 Dailler, Sylvain
1 Desharnais, Martin
1 Dubut, Jérémy
1 Džamonja, Mirna
1 Farjami, Ali
1 Fleury, Mathias
1 Gallois-Wong, Diane
1 Genestier, Richard
1 Guan, Yong
1 Hauzar, David
1 Hölzl, Johannes
1 Hriţcu, Cătălin
1 Kaliszyk, Cezary
1 Kang, Eunsuk
1 Kern, Kim
1 Klein, Gerwin
1 Koutsoukou-Argyraki, Angeliki
1 Kunčar, Ondřej
1 Lampropoulos, Leonidas
1 Lewis, Robert Y.
1 Li, Liming
1 Li, Yongdong
1 López Pombo, Carlos Gustavo
1 Ma, Sha
1 Marché, Claude
1 Martinez Suñé, Agustín Eloy
1 Meier, Fabian
1 Milicevic, Aleksandar
1 Möller, Bernhard
1 Momigliano, Alberto
1 Moy, Yannick
1 Near, Joseph P.
1 Ng, Yu-Chung
1 Owens, Scott
1 Pąk, Karol
1 Panny, Lorenz
1 Pease, Adam
1 Pierce, Benjamin C.
1 Raths, Thomas
1 Schmidt, Renate A.
1 Schreiner, Wolfgang
1 Schulz, Stephan
1 Sewell, Peter
1 Shao, Zhenzhou
1 Shi, Zhiping
1 Snelting, Gregor
1 Sternagel, Christian
1 Struth, Georg
1 Sutcliffe, Geoff
1 Thiemann, René
1 Tiemens, Lucca
1 Traytel, Dmitry
1 Urban, Josef
1 Waldmann, Uwe
1 Wand, Daniel
1 Weber, Leon
1 Wing, Jeannette Marie
1 Wisniewski, Max
1 Woodcock, James C. P.
...and 4 more Authors
all top 5

Cited in 15 Serials

11 Journal of Automated Reasoning
5 Journal of Logical and Algebraic Methods in Programming
3 Formal Aspects of Computing
2 Theory and Practice of Logic Programming
2 Logica Universalis
1 Acta Informatica
1 Artificial Intelligence
1 Bulletin of the Section of Logic
1 Experimental Mathematics
1 Formal Methods in System Design
1 Advances in Applied Clifford Algebras
1 Logic and Logical Philosophy
1 Mathematics in Computer Science
1 Logical Methods in Computer Science
1 Proceedings of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences
all top 5

Cited in 10 Fields

63 Computer science (68-XX)
36 Mathematical logic and foundations (03-XX)
2 Combinatorics (05-XX)
2 General algebraic systems (08-XX)
1 General and overarching topics; collections (00-XX)
1 History and biography (01-XX)
1 Linear and multilinear algebra; matrix theory (15-XX)
1 Category theory; homological algebra (18-XX)
1 Numerical analysis (65-XX)
1 Mechanics of particles and systems (70-XX)

Citations by Year