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.68326Blanchette, 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