×
Author ID: lammich.peter Recent zbMATH articles by "Lammich, Peter"
Published as: Lammich, Peter
Documents Indexed: 29 Publications since 2007, including 1 Book
Co-Authors: 20 Co-Authors with 20 Joint Publications
308 Co-Co-Authors

Publications by Year

Citations contained in zbMATH Open

24 Publications have been cited 207 times in 106 Documents Cited by Year
Applying data refinement for monadic programs to Hopcroft’s algorithm. Zbl 1360.68757
Lammich, Peter; Tuerk, Thomas
25
2012
Automatic data refinement. Zbl 1317.68216
Lammich, Peter
18
2013
Efficient verified (UN)SAT certificate checking. Zbl 1468.68133
Lammich, Peter
17
2017
Refinement to Imperative/HOL. Zbl 1465.68290
Lammich, Peter
16
2015
The Isabelle collections framework. Zbl 1291.68357
Lammich, Peter; Lochbihler, Andreas
13
2010
Verified efficient implementation of Gabow’s strongly connected component algorithm. Zbl 1416.68168
Lammich, Peter
13
2014
Formalizing the Edmonds-Karp algorithm. Zbl 1468.68327
Lammich, Peter; Sefidgar, S. Reza
10
2016
Refinement to imperative HOL. Zbl 1465.68291
Lammich, Peter
10
2019
Formal verification of an executable LTL model checker with partial order reduction. Zbl 1426.68162
Brunner, Julian; Lammich, Peter
10
2018
A verified SAT solver framework with learn, forget, restart, and incrementality. Zbl 1448.68457
Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph
9
2018
Predecessor sets of dynamic pushdown networks with tree-regular constraints. Zbl 1242.68058
Lammich, Peter; Müller-Olm, Markus; Wenner, Alexander
8
2009
Verified model checking of timed automata. Zbl 1423.68294
Wimmer, Simon; Lammich, Peter
8
2018
Efficient verified (UN)SAT certificate checking. Zbl 1468.68134
Lammich, Peter
8
2020
Generating verified LLVM from Isabelle/HOL. Zbl 07649971
Lammich, Peter
7
2019
Formalizing network flow algorithms: a refinement approach in Isabelle/HOL. Zbl 1468.68328
Lammich, Peter; Sefidgar, S. Reza
6
2019
Join-lock-sensitive forward reachability analysis for concurrent programs with dynamic process creation. Zbl 1317.68031
Gawlitza, Thomas Martin; Lammich, Peter; Müller-Olm, Markus; Seidl, Helmut; Wenner, Alexander
5
2011
Conflict analysis of programs with procedures, dynamic thread creation, and monitors. Zbl 1149.68355
Lammich, Peter; Müller-Olm, Markus
5
2008
Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol. Zbl 1284.68199
Schwarz, Martin D.; Seidl, Helmut; Vojdani, Vesal; Lammich, Peter; Müller-Olm, Markus
4
2011
Automatic refinement to efficient data structures: a comparison of two approaches. Zbl 1459.68228
Lammich, Peter; Lochbihler, Andreas
3
2019
Precise fixpoint-based analysis of programs with thread-creation and procedures. Zbl 1151.68361
Lammich, Peter; Müller-Olm, Markus
3
2007
Refinement with time – refining the run-time of algorithms in Isabelle/HOL. Zbl 07649969
Haslbeck, Maximilian P. L.; Lammich, Peter
3
2019
Proof pearl: Purely functional, simple and efficient priority search trees and applications to Prim and Dijkstra. Zbl 07649972
Lammich, Peter; Nipkow, Tobias
3
2019
Efficient verified implementation of introsort and pdqsort. Zbl 07614678
Lammich, Peter
2
2020
For a few dollars more. Verified fine-grained algorithm analysis down to LLVM. Zbl 1473.68222
Haslbeck, Maximilian P. L.; Lammich, Peter
1
2021
For a few dollars more. Verified fine-grained algorithm analysis down to LLVM. Zbl 1473.68222
Haslbeck, Maximilian P. L.; Lammich, Peter
1
2021
Efficient verified (UN)SAT certificate checking. Zbl 1468.68134
Lammich, Peter
8
2020
Efficient verified implementation of introsort and pdqsort. Zbl 07614678
Lammich, Peter
2
2020
Refinement to imperative HOL. Zbl 1465.68291
Lammich, Peter
10
2019
Generating verified LLVM from Isabelle/HOL. Zbl 07649971
Lammich, Peter
7
2019
Formalizing network flow algorithms: a refinement approach in Isabelle/HOL. Zbl 1468.68328
Lammich, Peter; Sefidgar, S. Reza
6
2019
Automatic refinement to efficient data structures: a comparison of two approaches. Zbl 1459.68228
Lammich, Peter; Lochbihler, Andreas
3
2019
Refinement with time – refining the run-time of algorithms in Isabelle/HOL. Zbl 07649969
Haslbeck, Maximilian P. L.; Lammich, Peter
3
2019
Proof pearl: Purely functional, simple and efficient priority search trees and applications to Prim and Dijkstra. Zbl 07649972
Lammich, Peter; Nipkow, Tobias
3
2019
Formal verification of an executable LTL model checker with partial order reduction. Zbl 1426.68162
Brunner, Julian; Lammich, Peter
10
2018
A verified SAT solver framework with learn, forget, restart, and incrementality. Zbl 1448.68457
Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph
9
2018
Verified model checking of timed automata. Zbl 1423.68294
Wimmer, Simon; Lammich, Peter
8
2018
Efficient verified (UN)SAT certificate checking. Zbl 1468.68133
Lammich, Peter
17
2017
Formalizing the Edmonds-Karp algorithm. Zbl 1468.68327
Lammich, Peter; Sefidgar, S. Reza
10
2016
Refinement to Imperative/HOL. Zbl 1465.68290
Lammich, Peter
16
2015
Verified efficient implementation of Gabow’s strongly connected component algorithm. Zbl 1416.68168
Lammich, Peter
13
2014
Automatic data refinement. Zbl 1317.68216
Lammich, Peter
18
2013
Applying data refinement for monadic programs to Hopcroft’s algorithm. Zbl 1360.68757
Lammich, Peter; Tuerk, Thomas
25
2012
Join-lock-sensitive forward reachability analysis for concurrent programs with dynamic process creation. Zbl 1317.68031
Gawlitza, Thomas Martin; Lammich, Peter; Müller-Olm, Markus; Seidl, Helmut; Wenner, Alexander
5
2011
Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol. Zbl 1284.68199
Schwarz, Martin D.; Seidl, Helmut; Vojdani, Vesal; Lammich, Peter; Müller-Olm, Markus
4
2011
The Isabelle collections framework. Zbl 1291.68357
Lammich, Peter; Lochbihler, Andreas
13
2010
Predecessor sets of dynamic pushdown networks with tree-regular constraints. Zbl 1242.68058
Lammich, Peter; Müller-Olm, Markus; Wenner, Alexander
8
2009
Conflict analysis of programs with procedures, dynamic thread creation, and monitors. Zbl 1149.68355
Lammich, Peter; Müller-Olm, Markus
5
2008
Precise fixpoint-based analysis of programs with thread-creation and procedures. Zbl 1151.68361
Lammich, Peter; Müller-Olm, Markus
3
2007
all top 5

Cited by 210 Authors

17 Lammich, Peter
11 Lochbihler, Andreas
9 Heule, Marijn J. H.
9 Nipkow, Tobias
4 Haslbeck, Maximilian P. L.
4 Schneider, Joshua P.
4 Traytel, Dmitry
3 Blanchette, Jasmin Christian
3 D’Souza, Deepak
3 D’Souza, Meenakshi
3 Marić, Filip
3 Müller-Olm, Markus
3 Myreen, Magnus O.
3 Norrish, Michael
3 Pai, Rekha R.
3 Schlichtkrull, Anders
3 Sefidgar, S. Reza
3 Seidl, Helmut
3 Touili, Tayssir
2 Abdulaziz, Mohammad
2 Aransay, Jesús
2 Atig, Mohamed Faouzi
2 Baek, Seulkee
2 Basin, David A.
2 Bouajjani, Ahmed
2 Brakensiek, Joshua
2 Brunner, Julian
2 Bryant, Randal E.
2 Divasón, Jose
2 Fleury, Mathias
2 Fürer, Basil
2 Guéneau, Armaël
2 Kumar, Ramana
2 Mackey, John
2 Michaelis, Julius
2 Narváez, David E.
2 Roßkopf, Simon
2 Singh, Abhishek
2 Tan, Yong Kiam
2 Théry, Laurent
2 Thiemann, René
2 van de Pol, Jan Cornelis
2 Weidenbach, Christoph
2 Wenner, Alexander
2 Wimmer, Simon
1 Abrahamsson, Oskar
1 Amani, Sidney
1 Banković, Milan
1 Barbosa, Haniel
1 Barrett, Clark W.
1 Biere, Armin
1 Bogaerts, Bart
1 Bøgsted Poulsen, Danny
1 Bordis, Tabea
1 Bromberger, Martin
1 Bulwahn, Lukas
1 Carle, Georg
1 Castaño, Fabian
1 Chakrabarti, Sujit Kumar
1 Charguéraud, Arthur
1 Chen, Ran
1 Chen, Zilin
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 Desharnais, Martin
1 Diekmann, Cornelius
1 Doczkal, Christian
1 Drecun, Ivan
1 Dupuis, Frédéric
1 Felgenhauer, Bertram
1 Foster, Jeffrey S.
1 Foster, Simon
1 Fu, Yu-Fu
1 Gammie, Peter
1 Gawlitza, Thomas Martin
1 Gleirscher, Mario
1 Gocht, Stephan
1 Goré, Rajeev Prabhakar
1 Gretton, Charles
1 Gross, Jason
1 Gupta, Aarti
1 Guttmann, Walter
1 Hanrot, Guillaume
1 Heimes, Lukas
1 Herbreteau, Frédéric
1 Ho, Son Lam
1 Hou, Ping
1 Huffman, Brian
1 Huisman, Marieke
1 Hunt, Warren jun.
1 Hupel, Lars
1 Immler, Fabian
1 Iordache, Viorel
1 Jackson, Vincent
1 Joosten, Sebastiaan J. C.
...and 110 more Authors

Citations by Year