Author of the publication

Verification Condition Generation for Permission Logics with Abstract Predicates and Abstraction Functions.

, , , and . ECOOP, volume 7920 of Lecture Notes in Computer Science, page 451-476. Springer, (2013)

Please choose a person to relate this publication to

To differ between persons with the same name, the academic degree and the title of an important publication will be displayed. You can also use the button next to the name to display some publications already assigned to the person.

 

Other publications of authors with the same name

The Relationship Between Separation Logic and Implicit Dynamic Frames, and . Logical Methods in Computer Science, (2012)Viper: A Verification Infrastructure for Permission-Based Reasoning., , and . Dependable Software Systems Engineering, volume 50 of NATO Science for Peace and Security Series - D: Information and Communication Security, IOS Press, (2017)Approaches to Polymorphism in Classical Sequent Calculus., and . ESOP, volume 3924 of Lecture Notes in Computer Science, page 84-99. Springer, (2006)The Relationship between Separation Logic and Implicit Dynamic Frames., and . ESOP, volume 6602 of Lecture Notes in Computer Science, page 439-458. Springer, (2011)Sound Automation of Magic Wands (extended version)., , , , and . CoRR, (2022)Modular Verification of Collaborating Smart Contracts., , , , and . CoRR, (2021)Formally Validating a Practical Verification Condition Generator., , and . CAV (2), volume 12760 of Lecture Notes in Computer Science, page 704-727. Springer, (2021)Prusti: deductive verification for Rust (keynote).. FTfJP@ECOOP, page 1. ACM, (2020)An Automatic Encoding from VeriFast Predicates into Implicit Dynamic Frames., and . VSTTE, volume 8164 of Lecture Notes in Computer Science, page 202-221. Springer, (2013)Rich specifications for Ethereum smart contract verification., , , , and . Proc. ACM Program. Lang., 5 (OOPSLA): 1-30 (2021)