Alexander J. Summers

CoRR, 2023

2022

Fractional resources in unbounded separation logic.

[BibT_eX]

[DOI]

Thibault Dardinier

Proc. ACM Program. Lang., 2022

REST: Integrating Term Rewriting with Program Verification (Artifact).

[BibT_eX]

[DOI]

Dagstuhl Artifacts Ser., 2022

Compositional Reasoning for Side-effectful Iterators and Iterator Adapters.

[BibT_eX]

[DOI]

CoRR, 2022

Sound Automation of Magic Wands (extended version).

[BibT_eX]

[DOI]

CoRR, 2022

REST: Integrating Term Rewriting with Program Verification (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2022

The Prusti Project: Formal Verification for Rust.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 14th International Symposium, 2022

REST: Integrating Term Rewriting with Program Verification.

[BibT_eX]

[DOI]

Proceedings of the 36th European Conference on Object-Oriented Programming, 2022

Sound Automation of Magic Wands.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 34th International Conference, 2022

Improving Linear Separability of Pulse Wave Laser Additive Manufacturing Classifiers with Rational Feature Engineering and Selection <sup>*</sup>.

[BibT_eX]

[DOI]

Proceedings of the American Control Conference, 2022

2021

Modular specification and verification of closures in Rust.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2021

Rich specifications for Ethereum smart contract verification.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2021

Formally Validating a Practical Verification Condition Generator (extended version).

[BibT_eX]

[DOI]

Gaurav Parthasarathy

CoRR, 2021

Modular Verification of Collaborating Smart Contracts.

[BibT_eX]

[DOI]

CoRR, 2021

Reframing the Liskov substitution principle through the lens of testing.

[BibT_eX]

[DOI]

Elisa L. A. Baniassad

Proceedings of the 2021 ACM SIGPLAN International Symposium on SPLASH-E, 2021

Formally Validating a Practical Verification Condition Generator.

[BibT_eX]

[DOI]

Gaurav Parthasarathy

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2020

Automating deductive verification for weak-memory programs (extended version).

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2020

How do programmers use unsafe rust?

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2020

Local Reasoning for Global Graph Properties.

[BibT_eX]

[DOI]

Siddharth Krishna

Thomas Wies

Proceedings of the Programming Languages and Systems, 2020

Prusti: deductive verification for Rust (keynote).

[BibT_eX]

[DOI]

Proceedings of the FTfJP 2020: Proceedings of the 22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs, 2020

2019

Modular verification of heap reachability properties in separation logic.

[BibT_eX]

[DOI]

Arshavir Ter-Gabrielyan

Proc. ACM Program. Lang., 2019

Leveraging rust types for modular specification and verification.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2019

The Axiom Profiler: Understanding and Debugging SMT Quantifier Instantiations.

[BibT_eX]

[DOI]

Nils Becker

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

2018

Automating Deductive Verification for Weak-Memory Programs.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

Permission Inference for Array Programs.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

2017

Viper: A Verification Infrastructure for Permission-Based Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Dependable Software Systems Engineering, 2017

2016

Viper: A Verification Infrastructure for Permission-Based Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

Actor Services - Modular Verification of Message Passing Programs.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2016

Automatic Verification of Iterated Separating Conjunctions Using Symbolic Execution.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 28th International Conference, 2016

2015

Lightweight Support for Magic Wands in an Automatic Verifier (Artifact).

[BibT_eX]

[DOI]

Dagstuhl Artifacts Ser., 2015

Software Verification "Across the Stack" (Invited Talk).

[BibT_eX]

[DOI]

Proceedings of the 29th European Conference on Object-Oriented Programming, 2015

Lightweight Support for Magic Wands in an Automatic Verifier.

[BibT_eX]

[DOI]

Proceedings of the 29th European Conference on Object-Oriented Programming, 2015

2014

Constraint Semantics for Abstract Read Permissions.

[BibT_eX]

[DOI]

Proceedings of 16th Workshop on Formal Techniques for Java-like Programs, 2014

2013

An Automatic Encoding from VeriFast Predicates into Implicit Dynamic Frames.

[BibT_eX]

[DOI]

Daniel Jost

Proceedings of the Verified Software: Theories, Tools, Experiments, 2013

Abstract Read Permissions: Fractional Permissions without the Fractions.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2013

A Formal Semantics for Isorecursive and Equirecursive State Abstractions.

[BibT_eX]

[DOI]

Proceedings of the ECOOP 2013 - Object-Oriented Programming, 2013

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

[BibT_eX]

[DOI]

Proceedings of the ECOOP 2013 - Object-Oriented Programming, 2013

2012

The Relationship Between Separation Logic and Implicit Dynamic Frames

[BibT_eX]

[DOI]

Matthew J. Parkinson

Log. Methods Comput. Sci., 2012

2011

Soundness and principal contexts for a shallow polymorphic type system based on classical logic.

[BibT_eX]

[DOI]

Log. J. IGPL, 2011

Freedom before commitment: a lightweight type system for object initialisation.

[BibT_eX]

[DOI]

Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2011

Fractional permissions without the fractions.

[BibT_eX]

[DOI]

Proceedings of the 13th Workshop on Formal Techniques for Java-Like Programs, 2011

2010

Considerate Reasoning and the Composite Design Pattern.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2010

Towards a semantic model for Java wildcards.

[BibT_eX]

[DOI]

Mariangiola Dezani-Ciancaglini

Nicholas Cameron

Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs, 2010

2009

Universe-Type-Based Verification Techniques for Mutable Static Fields and Methods.

[BibT_eX]

[DOI]

J. Object Technol., 2009

Modelling Java requires state.

[BibT_eX]

[DOI]

Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs, 2009

2008

Curry-Howard Term Calculi for Gentzen-Style Classical Logics.

[BibT_eX]

[DOI]

PhD thesis, 2008

A Unified Framework for Verification Techniques for Object Invariants.

[BibT_eX]

[DOI]

Proceedings of the Types, Logics and Semantics for State, 03.02. - 08.02.2008, 2008

2007

Pandora: A Reasoning Toolbox using Natural Deduction Style.

[BibT_eX]

[DOI]

Log. J. IGPL, 2007

Universe Types for Topology and Encapsulation.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Components and Objects, 6th International Symposium, 2007

2006

On the Computational Representation of Classical Logical Connectives.

[BibT_eX]

[DOI]

Jayshan Raghunandan

Proceedings of the Second International Workshop on Developments in Computational Models, 2006

Approaches to Polymorphism in Classical Sequent Calculus.

[BibT_eX]

[DOI]