Edit Profile (opens in new tab) Lammich, Peter Compute Distance To: Compute Author ID: lammich.peter Published as: Lammich, Peter Documents Indexed: 27 Publications since 2007, including 1 Book Co-Authors: 18 Co-Authors with 18 Joint Publications 289 Co-Co-Authors all top 5 Co-Authors 9 single-authored 6 Müller-Olm, Markus 2 Haslbeck, Maximilian P. L. 2 Lochbihler, Andreas 2 Sefidgar, S. Reza 2 Seidl, Helmut 2 Wenner, Alexander 1 Blanchette, Jasmin Christian 1 Brunner, Julian 1 Fleury, Mathias 1 Gawlitza, Thomas Martin 1 Hou, Ping 1 Nipkow, Tobias 1 Nordhoff, Benedikt 1 Schwarz, Martin D. 1 Tuerk, Thomas 1 Vojdani, Vesal 1 Weidenbach, Christoph 1 Wimmer, Simon Serials 7 Journal of Automated Reasoning Fields 27 Computer science (68-XX) 3 Combinatorics (05-XX) 2 Operations research, mathematical programming (90-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 18 Publications have been cited 143 times in 74 Documents Cited by ▼ Year ▼ Applying data refinement for monadic programs to Hopcroft’s algorithm. Zbl 1360.68757Lammich, Peter; Tuerk, Thomas 17 2012 Refinement to Imperative/HOL. Zbl 1465.68290Lammich, Peter 16 2015 Efficient verified (UN)SAT certificate checking. Zbl 1468.68133Lammich, Peter 15 2017 Automatic data refinement. Zbl 1317.68216Lammich, Peter 13 2013 Verified efficient implementation of Gabow’s strongly connected component algorithm. Zbl 1416.68168Lammich, Peter 12 2014 The Isabelle collections framework. Zbl 1291.68357Lammich, Peter; Lochbihler, Andreas 8 2010 Formal verification of an executable LTL model checker with partial order reduction. Zbl 1426.68162Brunner, Julian; Lammich, Peter 8 2018 Formalizing the Edmonds-Karp algorithm. Zbl 1468.68327Lammich, Peter; Sefidgar, S. Reza 8 2016 Refinement to imperative HOL. Zbl 1465.68291Lammich, Peter 7 2019 Predecessor sets of dynamic pushdown networks with tree-regular constraints. Zbl 1242.68058Lammich, Peter; Müller-Olm, Markus; Wenner, Alexander 7 2009 Verified model checking of timed automata. Zbl 1423.68294Wimmer, Simon; Lammich, Peter 6 2018 Join-lock-sensitive forward reachability analysis for concurrent programs with dynamic process creation. Zbl 1317.68031Gawlitza, Thomas Martin; Lammich, Peter; Müller-Olm, Markus; Seidl, Helmut; Wenner, Alexander 5 2011 A verified SAT solver framework with learn, forget, restart, and incrementality. Zbl 1448.68457Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph 5 2018 Formalizing network flow algorithms: a refinement approach in Isabelle/HOL. Zbl 1468.68328Lammich, Peter; Sefidgar, S. Reza 5 2019 Conflict analysis of programs with procedures, dynamic thread creation, and monitors. Zbl 1149.68355Lammich, Peter; Müller-Olm, Markus 4 2008 Efficient verified (UN)SAT certificate checking. Zbl 1468.68134Lammich, Peter 3 2020 Automatic refinement to efficient data structures: a comparison of two approaches. Zbl 1459.68228Lammich, Peter; Lochbihler, Andreas 2 2019 Precise fixpoint-based analysis of programs with thread-creation and procedures. Zbl 1151.68361Lammich, Peter; Müller-Olm, Markus 2 2007 Efficient verified (UN)SAT certificate checking. Zbl 1468.68134Lammich, Peter 3 2020 Refinement to imperative HOL. Zbl 1465.68291Lammich, Peter 7 2019 Formalizing network flow algorithms: a refinement approach in Isabelle/HOL. Zbl 1468.68328Lammich, Peter; Sefidgar, S. Reza 5 2019 Automatic refinement to efficient data structures: a comparison of two approaches. Zbl 1459.68228Lammich, Peter; Lochbihler, Andreas 2 2019 Formal verification of an executable LTL model checker with partial order reduction. Zbl 1426.68162Brunner, Julian; Lammich, Peter 8 2018 Verified model checking of timed automata. Zbl 1423.68294Wimmer, Simon; Lammich, Peter 6 2018 A verified SAT solver framework with learn, forget, restart, and incrementality. Zbl 1448.68457Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph 5 2018 Efficient verified (UN)SAT certificate checking. Zbl 1468.68133Lammich, Peter 15 2017 Formalizing the Edmonds-Karp algorithm. Zbl 1468.68327Lammich, Peter; Sefidgar, S. Reza 8 2016 Refinement to Imperative/HOL. Zbl 1465.68290Lammich, Peter 16 2015 Verified efficient implementation of Gabow’s strongly connected component algorithm. Zbl 1416.68168Lammich, Peter 12 2014 Automatic data refinement. Zbl 1317.68216Lammich, Peter 13 2013 Applying data refinement for monadic programs to Hopcroft’s algorithm. Zbl 1360.68757Lammich, Peter; Tuerk, Thomas 17 2012 Join-lock-sensitive forward reachability analysis for concurrent programs with dynamic process creation. Zbl 1317.68031Gawlitza, Thomas Martin; Lammich, Peter; Müller-Olm, Markus; Seidl, Helmut; Wenner, Alexander 5 2011 The Isabelle collections framework. Zbl 1291.68357Lammich, Peter; Lochbihler, Andreas 8 2010 Predecessor sets of dynamic pushdown networks with tree-regular constraints. Zbl 1242.68058Lammich, Peter; Müller-Olm, Markus; Wenner, Alexander 7 2009 Conflict analysis of programs with procedures, dynamic thread creation, and monitors. Zbl 1149.68355Lammich, Peter; Müller-Olm, Markus 4 2008 Precise fixpoint-based analysis of programs with thread-creation and procedures. Zbl 1151.68361Lammich, Peter; Müller-Olm, Markus 2 2007 all cited Publications top 5 cited Publications all top 5 Cited by 145 Authors 14 Lammich, Peter 10 Lochbihler, Andreas 7 Heule, Marijn J. H. 5 Nipkow, Tobias 4 Haslbeck, Maximilian P. L. 4 Schneider, Joshua P. 4 Traytel, Dmitry 3 Blanchette, Jasmin Christian 3 Myreen, Magnus O. 3 Norrish, Michael 3 Sefidgar, S. Reza 2 Abdulaziz, Mohammad 2 Aransay, Jesús 2 Baek, Seulkee 2 Basin, David A. 2 Brakensiek, Joshua 2 Brunner, Julian 2 Divasón, Jose 2 Fürer, Basil 2 Guéneau, Armaël 2 Kumar, Ramana 2 Mackey, John 2 Marić, Filip 2 Müller-Olm, Markus 2 Narváez, David E. 2 Schlichtkrull, Anders 2 Seidl, Helmut 2 Tan, Yong Kiam 2 Théry, Laurent 2 Touili, Tayssir 2 Wenner, Alexander 1 Abrahamsson, Oskar 1 Atig, Mohamed Faouzi 1 Barbosa, Haniel 1 Barrett, Clark W. 1 Biere, Armin 1 Bouajjani, Ahmed 1 Bryant, Randal E. 1 Bulwahn, Lukas 1 Carle, Georg 1 Charguéraud, Arthur 1 Chen, Ran 1 Chlipala, Adam J. 1 Ciobâcă, Ştefan 1 Cohen, Cyril 1 Cruz-Filipe, Luís 1 Dabrowski, Frédéric 1 Dardinier, Thibault 1 Delaware, Benjamin 1 Diekmann, Cornelius 1 Doczkal, Christian 1 Felgenhauer, Bertram 1 Fleury, Mathias 1 Foster, Jeffrey S. 1 Foster, Simon 1 Fu, Yu-Fu 1 Futatsugi, Kokichi 1 Gammie, Peter 1 Gawlitza, Thomas Martin 1 Gleirscher, Mario 1 Goré, Rajeev Prabhakar 1 Gretton, Charles 1 Gross, Jason 1 Gupta, Aarti 1 Hanrot, Guillaume 1 Heimes, Lukas 1 Herbreteau, Frédéric 1 Ho, Son Lam 1 Hobor, Aquinas 1 Hou, Ping 1 Hupel, Lars 1 Immler, Fabian 1 Iordache, Viorel 1 Jourdan, Jacques-Henri 1 Kahlon, Vineet 1 Kanabar, Hrutvik 1 Kelly, Tim 1 Kiesl, Benjamin 1 Kobayashi, Naoki 1 Konečný, Michal 1 Kremer, Gereon 1 Krstić, Srđan 1 Lachnitt, Hanna 1 Leow, Wei Xiang 1 Levy, Jean-Jacques 1 Liu, Jiaxiang 1 Lugiez, Denis 1 Lumezanu, Cristian 1 Mantel, Heiko 1 Marques-Silva, João P. 1 Martin-Dorel, Érik 1 Matichuk, Daniel 1 Mayero, Micaela 1 Mehlhorn, Kurt 1 Merz, Stephan 1 Michaelis, Julius 1 Mohan, Anshuman 1 Muscholl, Anca 1 Narayan, Kumar K. 1 Nemouchi, Yakoub ...and 45 more Authors Cited in 5 Serials 21 Journal of Automated Reasoning 3 Formal Aspects of Computing 2 Information and Computation 2 Logical Methods in Computer Science 1 Journal of Cryptology all top 5 Cited in 13 Fields 73 Computer science (68-XX) 7 Mathematical logic and foundations (03-XX) 5 Combinatorics (05-XX) 3 Numerical analysis (65-XX) 2 Linear and multilinear algebra; matrix theory (15-XX) 2 Convex and discrete geometry (52-XX) 2 Operations research, mathematical programming (90-XX) 2 Information and communication theory, circuits (94-XX) 1 Category theory; homological algebra (18-XX) 1 Ordinary differential equations (34-XX) 1 Dynamical systems and ergodic theory (37-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 Biology and other natural sciences (92-XX) Citations by Year