×

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; Isabelle; Coq; TPTP; HOL; z3; LEO-II; PVS; Satallax; Archive Formal Proofs; E Theorem Prover; HOL Light; Kodkod; SmallCheck; QuickCheck; Mizar; VAMPIRE; CVC4; SPASS
Referenced in: 64 Publications
all top 5

Referenced by 96 Authors

19 Benzmüller, Christoph Ewald
11 Blanchette, Jasmin Christian
7 Guttmann, Walter
4 Paulson, Lawrence Charles
4 Reynolds, Andrew
4 Woltzenlogel Paleo, Bruno
3 Fuenmayor, David
3 Nipkow, Tobias
3 Parent, Xavier
3 Steen, Alexander
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 Lochbihler, Andreas
2 Norrish, Michael
2 Pease, Alison
2 Popescu, Andrei
2 Raggi, Daniel
2 Tinelli, Cesare
2 van der Torre, Leendert W. N.
2 Wenzel, Makarius
1 Avigad, Jeremy
1 Barrett, Clark W.
1 Baumgartner, Peter
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 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 Kunčar, Ondřej
1 Lampropoulos, Leonidas
1 Lewis, Robert Y.
1 Li, Liming
1 Li, Yongdong
1 Ma, Sha
1 Marché, Claude
1 Meier, Fabian
1 Milicevic, Aleksandar
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 Scott, Dana Stewart
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 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.
1 Wu, Minchao
1 Xia, Li-Yao
1 Yamada, Akihisa
1 Zappa Nardelli, Francesco

Referencing Publications by Year