×

zbMATH — the first resource for mathematics

Leino, K. Rustan M.

Compute Distance To:
Author ID: leino.k-rustan-m Recent zbMATH articles by "Leino, K. Rustan M."
Published as: Leino, K. Rustan M.; Leino, M.
Homepage: http://www.mathmeth.com/leino/
External Links: MGP
Documents Indexed: 38 Publications since 1988, including 2 Books

Publications by Year

Citations contained in zbMATH Open

29 Publications have been cited 168 times in 134 Documents Cited by Year
Dafny: an automatic program verifier for functional correctness. Zbl 1253.68095
Leino, K. Rustan M.
31
2010
A semantic approach to secure information flow. Zbl 0954.68052
Joshi, Rajeev; Leino, K. Rustan M.
18
2000
Specification and verification challenges for sequential object-oriented programs. Zbl 1121.68074
Leavens, Gary T.; Leino, K. Rustan M.; Müller, Peter
12
2007
Houdini, an annotation assistant for ESC/Java. Zbl 0977.68671
Flanagan, Cormac; Leino, K. Rustan M.
12
2001
A logic of object-oriented programs. Zbl 1274.68055
Abadi, Martín; Leino, K. Rustan M.
11
2003
Efficient weakest preconditions. Zbl 1173.68563
Leino, K. Rustan M.
10
2005
Loop invariants on demand. Zbl 1159.68374
Leino, K. Rustan M.; Logozzo, Francesco
10
2005
A basis for verifying multi-threaded programs. Zbl 1234.68078
Leino, K. Rustan M.; Müller, Peter
9
2009
HOL-Boogie – an interactive prover for the Boogie program-verifier. Zbl 1165.68399
Böhme, Sascha; Leino, K. Rustan M.; Wolff, Burkhart
7
2008
Abstract interpretation with alien expressions and heap structures. Zbl 1111.68397
Chang, Bor-Yuh Evan; Leino, K. Rustan M.
6
2005
Recursive object types in a logic of object-oriented programs. Zbl 0913.68025
Leino, K. Rustan M.
6
1998
Behavioral interface specification languages. Zbl 1293.68078
Hatcliff, John; Leavens, Gary T.; Leino, K. Rustan M.; Müller, Peter; Parkinson, Matthew
5
2012
A polymorphic intermediate verification language: design and logical encoding. Zbl 1284.68409
Leino, K. Rustan M.; Rümmer, Philipp
5
2010
Modular verification of static class invariants. Zbl 1120.68377
Leino, K. Rustan M.; Müller, Peter
4
2005
Generating error traces from verification-condition counterexamples. Zbl 1075.68018
Leino, K. Rustan M.; Millstein, Todd; Saxe, James B.
4
2005
A verification methodology for model fields. Zbl 1178.68348
Leino, K. Rustan M.; Müller, Peter
3
2006
Automating induction with an SMT solver. Zbl 1326.68262
Leino, K. Rustan M.
2
2012
Virginity: A contribution to the specification of object-oriented software. Zbl 1002.68025
Leino, K. Rustan M.; Stata, Raymie
2
1999
An assertional proof of the stability and correctness of Natural Mergesort. Zbl 1367.68080
Leino, K. Rustan M.; Lucio, Paqui
1
2015
Automating theorem proving with SMT. Zbl 1317.68217
Leino, K. Rustan M.
1
2013
Tools and algorithms for the construction and analysis of systems. 17th international conference, TACAS 2011, held as part of the joint European conferences on theory and practice of software, ETAPS 2011, Saarbrücken, Germany, March 26 – April 3, 2011. Proceedings. Zbl 1213.68016
Abdulla, Parosh Aziz (ed.); Leino, K. Rustan M. (ed.)
1
2011
Doomed program points. Zbl 1211.68090
Hoenicke, Jochen; Leino, K. Rustan M.; Podelski, Andreas; Schäf, Martin; Wies, Thomas
1
2010
Verification of equivalent-results methods. Zbl 1133.68377
Leino, K. Rustan M.; Müller, Peter
1
2008
A verifying compiler for a multi-threaded object-oriented language. Zbl 1153.68016
Leino, K. Rustan M.; Schulte, Wolfram
1
2007
Using history invariants to verify observers. Zbl 1187.68156
Leino, K. Rustan M.; Schulte, Wolfram
1
2007
A SAT characterization of Boolean-program correctness. Zbl 1023.68534
Leino, K. Rustan M.
1
2003
Applications of extended static checking. Zbl 0997.68562
Leino, K. Rustan M.
1
2001
Joining specification statements. Zbl 0914.68127
Rustan, K.; Leino, M.; Manohar, Rajit
1
1999
Extremal solutions for regularizing ill-posed problems. Zbl 0662.65114
Paatero, P.; Leino, M.
1
1988
An assertional proof of the stability and correctness of Natural Mergesort. Zbl 1367.68080
Leino, K. Rustan M.; Lucio, Paqui
1
2015
Automating theorem proving with SMT. Zbl 1317.68217
Leino, K. Rustan M.
1
2013
Behavioral interface specification languages. Zbl 1293.68078
Hatcliff, John; Leavens, Gary T.; Leino, K. Rustan M.; Müller, Peter; Parkinson, Matthew
5
2012
Automating induction with an SMT solver. Zbl 1326.68262
Leino, K. Rustan M.
2
2012
Tools and algorithms for the construction and analysis of systems. 17th international conference, TACAS 2011, held as part of the joint European conferences on theory and practice of software, ETAPS 2011, Saarbrücken, Germany, March 26 – April 3, 2011. Proceedings. Zbl 1213.68016
Abdulla, Parosh Aziz (ed.); Leino, K. Rustan M. (ed.)
1
2011
Dafny: an automatic program verifier for functional correctness. Zbl 1253.68095
Leino, K. Rustan M.
31
2010
A polymorphic intermediate verification language: design and logical encoding. Zbl 1284.68409
Leino, K. Rustan M.; Rümmer, Philipp
5
2010
Doomed program points. Zbl 1211.68090
Hoenicke, Jochen; Leino, K. Rustan M.; Podelski, Andreas; Schäf, Martin; Wies, Thomas
1
2010
A basis for verifying multi-threaded programs. Zbl 1234.68078
Leino, K. Rustan M.; Müller, Peter
9
2009
HOL-Boogie – an interactive prover for the Boogie program-verifier. Zbl 1165.68399
Böhme, Sascha; Leino, K. Rustan M.; Wolff, Burkhart
7
2008
Verification of equivalent-results methods. Zbl 1133.68377
Leino, K. Rustan M.; Müller, Peter
1
2008
Specification and verification challenges for sequential object-oriented programs. Zbl 1121.68074
Leavens, Gary T.; Leino, K. Rustan M.; Müller, Peter
12
2007
A verifying compiler for a multi-threaded object-oriented language. Zbl 1153.68016
Leino, K. Rustan M.; Schulte, Wolfram
1
2007
Using history invariants to verify observers. Zbl 1187.68156
Leino, K. Rustan M.; Schulte, Wolfram
1
2007
A verification methodology for model fields. Zbl 1178.68348
Leino, K. Rustan M.; Müller, Peter
3
2006
Efficient weakest preconditions. Zbl 1173.68563
Leino, K. Rustan M.
10
2005
Loop invariants on demand. Zbl 1159.68374
Leino, K. Rustan M.; Logozzo, Francesco
10
2005
Abstract interpretation with alien expressions and heap structures. Zbl 1111.68397
Chang, Bor-Yuh Evan; Leino, K. Rustan M.
6
2005
Modular verification of static class invariants. Zbl 1120.68377
Leino, K. Rustan M.; Müller, Peter
4
2005
Generating error traces from verification-condition counterexamples. Zbl 1075.68018
Leino, K. Rustan M.; Millstein, Todd; Saxe, James B.
4
2005
A logic of object-oriented programs. Zbl 1274.68055
Abadi, Martín; Leino, K. Rustan M.
11
2003
A SAT characterization of Boolean-program correctness. Zbl 1023.68534
Leino, K. Rustan M.
1
2003
Houdini, an annotation assistant for ESC/Java. Zbl 0977.68671
Flanagan, Cormac; Leino, K. Rustan M.
12
2001
Applications of extended static checking. Zbl 0997.68562
Leino, K. Rustan M.
1
2001
A semantic approach to secure information flow. Zbl 0954.68052
Joshi, Rajeev; Leino, K. Rustan M.
18
2000
Virginity: A contribution to the specification of object-oriented software. Zbl 1002.68025
Leino, K. Rustan M.; Stata, Raymie
2
1999
Joining specification statements. Zbl 0914.68127
Rustan, K.; Leino, M.; Manohar, Rajit
1
1999
Recursive object types in a logic of object-oriented programs. Zbl 0913.68025
Leino, K. Rustan M.
6
1998
Extremal solutions for regularizing ill-posed problems. Zbl 0662.65114
Paatero, P.; Leino, M.
1
1988
all top 5

Cited by 306 Authors

6 Böhme, Sascha
5 Leino, K. Rustan M.
5 Wolff, Burkhart
4 Lahiri, Shuvendu Kumar
4 Weiss, Benjamin
3 Banerjee, Anindya
3 Beringer, Lennart
3 Blanchette, Jasmin Christian
3 Charlton, Nathaniel
3 de Boer, Frank S.
3 Hähnle, Reiner
3 Hermenegildo, Manuel V.
3 Kröning, Daniel
3 Marché, Claude
3 Morgan, Carroll C.
3 Naumann, David A.
3 Pinto, Jorge Sousa
3 Ulbrich, Mattias
2 Barthe, Gilles
2 Brucker, Achim D.
2 Dovland, Johan
2 Ferrara, Pietro
2 Frade, Maria João
2 Furia, Carlo Alberto
2 Garg, Pranav
2 Huth, Michael R. A.
2 Jacobs, Bart
2 Johnsen, Einar Broch
2 Liu, Zhiming
2 Madhusudan, Parthasarathy
2 Mastroeni, Isabella
2 McIver, Annabelle K.
2 Meyer, Bertrand
2 Morales, Jose Francisco
2 Moskal, Michał
2 Moy, Yannick
2 Neider, Daniel
2 O’Hearn, Peter W.
2 Owe, Olaf
2 Paskevich, Andrei
2 Piessens, Frank
2 Popescu, Andrei
2 Reddy, Uday S.
2 Reus, Bernhard
2 Schmitt, Peter H.
2 Schulte, Wolfram
2 Sharygina, Natasha
2 Shoham, Sharon
2 Smallbone, Nicholas
2 Steffen, Martin
1 Abujarad, Fuad
1 Ah-Fat, Patrick
1 Ahrendt, Wolfgang
1 Alkassar, Eyad
1 Amighi, Afshin
1 Appel, Andrew W.
1 Apt, Krzysztof Rafal
1 Armstrong, Alasdair
1 Aspinall, David
1 Bacelar Almeida, José
1 Bao, Yuyan
1 Barbosa, Manuel
1 Barnes, Janet
1 Barnett, Mike
1 Beckert, Bernhard
1 Berger, Martin J.
1 Bijlsma, Lex
1 Bjørner, Nikolaj S.
1 Blom, Stefan
1 Bobot, François
1 Bodik, Rastislav
1 Boström, Pontus
1 Boulmé, Sylvain
1 Bouzy, Aymeric
1 Boyland, John Tang
1 Brenas, Jon Haël
1 Bruns, Daniel
1 Bsaïes, Khaled
1 Bubel, Richard
1 Bueno, Francisco
1 Cao, Qinxiang
1 Carro, Manuel
1 Chalin, Patrice
1 Chang, Carolina
1 Chapman, Roderick
1 Charguéraud, Arthur
1 Chechik, Marsha
1 Chen, Hao
1 Chimento, Jesús Mauricio
1 Claessen, Koen
1 Clarkson, Michael R.
1 Colvin, Robert J.
1 Cook, Andrew W.
1 Cook, Byron
1 Crespo, Juan Manuel
1 da Costa, Umberto Souza
1 Dailler, Sylvain
1 Damiani, Ferruccio
1 Darabi, Saeed
1 D’Argenio, Pedro Rubén
...and 206 more Authors

Citations by Year