Peter Müller

Formal Aspects Comput., June, 2023

Verification-Preserving Inlining in Automatic Separation Logic Verifiers.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., April, 2023

Leveraging Rust Types for Program Synthesis.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2023

CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2023

Theoretical Advances and Emerging Applications in Abstract Interpretation (Dagstuhl Seminar 23281).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2023

Refinement Proofs in Rust Using Ghost Locks.

[BibT_eX]

[DOI]

CoRR, 2023

Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version).

[BibT_eX]

[DOI]

CoRR, 2023

Sound Verification of Security Protocols: From Design to Interoperable Implementations.

[BibT_eX]

[DOI]

Proceedings of the 44th IEEE Symposium on Security and Privacy, 2023

A Generic Methodology for the Modular Verification of Security Protocol Implementations.

[BibT_eX]

[DOI]

Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security, 2023

2022

Concise outlines for a complex logic: a proof outline checker for TaDA.

[BibT_eX]

[DOI]

Felix A. Wolf

Formal Methods Syst. Des., August, 2022

The Complete Guide to SCION - From Design Principles to Formal Verification

[BibT_eX]

[DOI]

Information Security and Cryptography, Springer, ISBN: 978-3-031-05288-0, 2022

Fractional resources in unbounded separation logic.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2022

Sound Verification of Security Protocols: From Design to Interoperable Implementations (extended version).

[BibT_eX]

[DOI]

CoRR, 2022

Compositional Reasoning for Side-effectful Iterators and Iterator Adapters.

[BibT_eX]

[DOI]

CoRR, 2022

Verification-Preserving Inlining in Automatic Separation Logic Verifiers (extended version).

[BibT_eX]

[DOI]

CoRR, 2022

Sound Automation of Magic Wands (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

Sound Automation of Magic Wands.

[BibT_eX]

[DOI]

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

2021

Introduction to the Special Section on ESOP 2020.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2021

VerifyThis 2019: a program verification competition.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 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

Flexible Refinement Proofs in Separation Logic.

[BibT_eX]

[DOI]

Aurel Bílý

Christoph Matheja

CoRR, 2021

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

[BibT_eX]

[DOI]

CoRR, 2021

Gobra: Modular Specification and Verification of Go Programs (extended version).

[BibT_eX]

[DOI]

CoRR, 2021

Modular Verification of Collaborating Smart Contracts.

[BibT_eX]

[DOI]

CoRR, 2021

Identifying Overly Restrictive Matching Patterns in SMT-Based Program Verifiers.

[BibT_eX]

[DOI]

Alexandra Bugariu

Arshavir Ter-Gabrielyan

Proceedings of the Formal Methods - 24th International Symposium, 2021

Gobra: Modular Specification and Verification of Go Programs.

[BibT_eX]

[DOI]

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

Formally Validating a Practical Verification Condition Generator.

[BibT_eX]

[DOI]

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

Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security.

[BibT_eX]

[DOI]

Severin Meier

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

The First Fifteen Years of the Verified Software Project.

[BibT_eX]

[DOI]

Natarajan Shankar

Proceedings of the Theories of Programming: The Life and Works of Tony Hoare, 2021

2020

Modular Product Programs.

[BibT_eX]

[DOI]

Samuel Hitz

ACM Trans. Program. Lang. Syst., 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

Igloo: soundly linking compositional refinement and separation logic for distributed system verification.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2020

Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA (Full Paper).

[BibT_eX]

[DOI]

Felix A. Wolf

CoRR, 2020

VerifyThis 2019: A Program Verification Competition (Extended Report).

[BibT_eX]

[DOI]

CoRR, 2020

Automatically testing string solvers.

[BibT_eX]

[DOI]

Alexandra Bugariu

Proceedings of the ICSE '20: 42nd International Conference on Software Engineering, Seoul, South Korea, 27 June, 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

Specification Mining for Smart Contracts with Automatic Abstraction Tuning.

[BibT_eX]

[DOI]

CoRR, 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

Abstract Interpretation of CTL Properties.

[BibT_eX]

[DOI]

Caterina Urban

Samuel Ueltschi

Proceedings of the Static Analysis - 25th International Symposium, 2018

Static serializability analysis for causal consistency.

[BibT_eX]

[DOI]

Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018

Automatically testing implementations of numerical abstract domains.

[BibT_eX]

[DOI]

Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, 2018

An Abstract Interpretation Framework for Input Data Usage.

[BibT_eX]

[DOI]

Caterina Urban

Proceedings of the Programming Languages and Systems, 2018

MaxSMT-Based Type Inference for Python 3.

[BibT_eX]

[DOI]

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

Nagini: A Static Verifier for Python.

[BibT_eX]

[DOI]

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

Permission Inference for Array Programs.

[BibT_eX]

[DOI]

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

The Binomial Heap Verification Challenge in Viper.

[BibT_eX]

[DOI]

Proceedings of the Principled Software Development, 2018

2017

Viper: A Verification Infrastructure for Permission-Based Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Dependable Software Systems Engineering, 2017

Serializability for eventual consistency: criterion, analysis, and applications.

[BibT_eX]

[DOI]

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

A general framework for dynamic stub injection.

[BibT_eX]

[DOI]

Proceedings of the 39th International Conference on Software Engineering, 2017

Precise Version Control of Trees with Line-Based Version Control Systems.

[BibT_eX]

[DOI]

Proceedings of the Fundamental Approaches to Software Engineering, 2017

2016

Synergies among Testing, Verification, and Repair for Concurrent Programs (Dagstuhl Seminar 16201).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2016

The IDE as a Scriptable Information System (extended version).

[BibT_eX]

[DOI]

Lukas Vogel

CoRR, 2016

Viper: A Verification Infrastructure for Permission-Based Reasoning.

[BibT_eX]

[DOI]

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

Diagnostic Information for Control-Flow Analysis of Workflow Graphs (a.k.a. Free-Choice Workflow Nets).

[BibT_eX]

[DOI]

Cédric Favre

Hagen Völzer

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

Integrated Environment for Diagnosing Verification Errors.

[BibT_eX]

[DOI]

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

The IDE as a scriptable information system.

[BibT_eX]

[DOI]

Lukas Vogel

Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, 2016

Guiding dynamic symbolic execution toward unverified program executions.

[BibT_eX]

[DOI]

Proceedings of the 38th International Conference on Software Engineering, 2016

Actor Services - Modular Verification of Message Passing Programs.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2016

The Effect of Richer Visualizations on Code Comprehension.

[BibT_eX]

[DOI]

Otmar Hilliges

Proceedings of the 2016 CHI Conference on Human Factors in Computing 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

Automatic Inference of Heap Properties Exploiting Value Domains.

[BibT_eX]

[DOI]

Milos Novácek

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

An Experimental Evaluation of Deliberate Unsoundness in a Static Program Analyzer.

[BibT_eX]

[DOI]

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

Building automatic program verifiers.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages Mentoring Workshop, 2015

Modular Verification of Finite Blocking in Non-terminating Programs.

[BibT_eX]

[DOI]

Pontus Boström

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

2014

Envision: A fast and flexible visual code editor with fluid interactions (Overview).

[BibT_eX]

[DOI]

Proceedings of the IEEE Symposium on Visual Languages and Human-Centric Computing, 2014

Synthesizing Parameterized Unit Tests to Detect Object Invariant Violations.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering and Formal Methods - 12th International Conference, 2014

Dynamic Test Generation with Static Fields and Initializers.

[BibT_eX]

[DOI]

Patrick Emmisberger

Proceedings of the Runtime Verification - 5th International Conference, 2014

TouchGuru: Integrating Static Analysis with a Mobile Development Environment.

[BibT_eX]

[DOI]

Lucas Brutschy

Proceedings of the 2nd International Workshop on Mobile Development Lifecycle, 2014

Static analysis for independent app developers.

[BibT_eX]

[DOI]

Lucas Brutschy

Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, 2014

Constraint Semantics for Abstract Read Permissions.

[BibT_eX]

[DOI]

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

2013

Object Ownership in Program Verification.

[BibT_eX]

[DOI]

Proceedings of the Aliasing in Object-Oriented Programming. Types, 2013

Abstract Read Permissions: Fractional Permissions without the Fractions.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2013

Customizing the visualization and interaction for embedded domain-specific languages in a structured editor.

[BibT_eX]

[DOI]

Proceedings of the 2013 IEEE Symposium on Visual Languages and Human Centric Computing, 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

Behavioral interface specification languages.

[BibT_eX]

[DOI]

ACM Comput. Surv., 2012

Comparing Verification Condition Generation with Symbolic Execution: An Experience Report.

[BibT_eX]

[DOI]

Ioannis T. Kassios

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

Automatic Inference of Access Permissions.

[BibT_eX]

[DOI]

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

Collaborative Verification and Testing with Explicit Assumptions.

[BibT_eX]

[DOI]

Proceedings of the FM 2012: Formal Methods, 2012

2011

Formal Methods-Based Tools for Race, Deadlock, and Other Errors.

[BibT_eX]

[DOI]

Proceedings of the Encyclopedia of Parallel Computing, 2011

Separating ownership topology and encapsulation with generic universe types.

[BibT_eX]

[DOI]

Sophia Drossopoulou

ACM Trans. Program. Lang. Syst., 2011

Specification and verification: the Spec# experience.

[BibT_eX]

[DOI]

Commun. ACM, 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

Using Debuggers to Understand Failed Verification Attempts.

[BibT_eX]

[DOI]

Joseph N. Ruskiewicz

Proceedings of the FM 2011: Formal Methods, 2011

The 1st Verified Software Competition: Experience Report.

[BibT_eX]

[DOI]

Proceedings of the FM 2011: Formal Methods, 2011

Fractional permissions without the fractions.

[BibT_eX]

[DOI]

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

Tunable Static Inference for Generic Universe Types.

[BibT_eX]

[DOI]

Michael D. Ernst

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

2010

Reasoning about Function Objects.

[BibT_eX]

[DOI]

Proceedings of the Objects, Models, Components, Patterns, 48th International Conference, 2010

Efficient Runtime Assertion Checking of Assignable Clauses with Datagroups.

[BibT_eX]

[DOI]

Hermann Lehner

Proceedings of the Fundamental Approaches to Software Engineering, 2010

Proving Consistency and Completeness of Model Classes Using Theory Interpretation.

[BibT_eX]

[DOI]

Proceedings of the Fundamental Approaches to Software Engineering, 2010

Deadlock-Free Channels and Locks.

[BibT_eX]

[DOI]

Jan Smans

Proceedings of the Programming Languages and Systems, 2010

2009

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

[BibT_eX]

[DOI]

Sophia Drossopoulou

J. Object Technol., 2009

A Sound and Complete Program Logic for Eiffel.

[BibT_eX]

[DOI]

Proceedings of the Objects, Components, Models and Patterns, 47th International Conference, 2009

Verification of Concurrent Programs with Chalice.

[BibT_eX]

[DOI]

Jan Smans

Proceedings of the Foundations of Security Analysis and Design V, 2009

A Basis for Verifying Multi-threaded Programs.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2009

A Modular Verification Methodology for C# Delegates.

[BibT_eX]

[DOI]

Joseph N. Ruskiewicz

Proceedings of the Rigorous Methods for Software Construction and Analysis, 2009

2008

Faithful mapping of model classes to mathematical structures.

[BibT_eX]

[DOI]

IET Softw., 2008

Flexible Immutability with Frozen Objects.

[BibT_eX]

[DOI]

Angela Wallenburg

Proceedings of the Verified Software: Theories, 2008

Proof-Transforming Compilation of Eiffel Programs.

[BibT_eX]

[DOI]

Martin Nordio

Bertrand Meyer

Proceedings of the Objects, Components, Models and Patterns, 46th International Conference, 2008

Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs.

[BibT_eX]

[DOI]

Proceedings of the Advanced Lectures on Software Engineering, 2008

Checking Well-Formedness of Pure-Method Specifications.

[BibT_eX]

[DOI]

Arsenii Rudich

Proceedings of the FM 2008: Formal Methods, 2008

Verification of Equivalent-Results Methods.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2008

Aliasing, Confinement, and Ownership in Object-Oriented Programming.

[BibT_eX]

[DOI]

Proceedings of the Object-Oriented Technology. ECOOP 2008 Workshop Reader, 2008

Formal Techniques for Java-Like Programs.

[BibT_eX]

[DOI]

Proceedings of the Object-Oriented Technology. ECOOP 2008 Workshop Reader, 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

Specification and verification challenges for sequential object-oriented programs.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2007

Formal Translation of Bytecode into BoogiePL.

[BibT_eX]

[DOI]

Hermann Lehner

Proceedings of the Second Workshop on Bytecode Semantics, 2007

Proof-transforming compilation of programs with abrupt termination.

[BibT_eX]

[DOI]

Martin Nordio

Proceedings of the 2007 Conference Specification and Verification of Component-Based Systems, 2007

Sound reasoning about unchecked exceptions.

[BibT_eX]

[DOI]

Bart Jacobs

Frank Piessens

Proceedings of the Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 2007

Ownership transfer in universe types.

[BibT_eX]

[DOI]

Arsenii Rudich

Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2007

Information Hiding and Visibility in Interface Specifications.

[BibT_eX]

[DOI]

Proceedings of the 29th International Conference on Software Engineering (ICSE 2007), 2007

Universe Types for Topology and Encapsulation.

[BibT_eX]

[DOI]

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

Generic Universe Types.

[BibT_eX]

[DOI]

Sophia Drossopoulou

Proceedings of the ECOOP 2007 - Object-Oriented Programming, 21st European Conference, Berlin, Germany, July 30, 2007

07091 Abstracts Collection - Mobility, Ubiquity and Security.

[BibT_eX]

[DOI]

Proceedings of the Mobility, Ubiquity and Security, 25.02. - 02.03.2007, 2007

07091 Executive Summary - Mobility, Ubiquity and Security.

[BibT_eX]

[DOI]

Proceedings of the Mobility, Ubiquity and Security, 25.02. - 02.03.2007, 2007

2006

Modular invariants for layered object structures.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2006

Reasoning About Method Calls in Interface Specifications.

[BibT_eX]

[DOI]

J. Object Technol., 2006

MOBIUS: Mobility, Ubiquity, Security.

[BibT_eX]

[DOI]

Proceedings of the Trustworthy Global Computing, Second Symposium, 2006

Changing Programs Correctly: Refactoring with Specifications.

[BibT_eX]

[DOI]

Fabian Bannwart

Proceedings of the FM 2006: Formal Methods, 2006

A Pattern Language for Overlay Networks in Peer-to-Peer Systems.

[BibT_eX]

Dominik Grolimund

Proceedings of the EuroPLoP' 2006, 2006

A Verification Methodology for Model Fields.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2006

2005

Universes: Lightweight Ownership for JML.

[BibT_eX]

[DOI]

J. Object Technol., 2005

A Program Logic for Bytecode.

[BibT_eX]

[DOI]

Fabian Bannwart

Proceedings of the First Workshop on Bytecode Semantics, 2005

Reasoning about Object Structures Using Ownership.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, 2005

Modular Verification of Static Class Invariants.

[BibT_eX]

[DOI]

Proceedings of the FM 2005: Formal Methods, 2005

2004

Formal Techniques for Java-Like Programs (FTfJP).

[BibT_eX]

[DOI]

Proceedings of the Object-Oriented Technology: ECOOP 2004 Workshop Reader, 2004

Object Invariants in Dynamic Contexts.

[BibT_eX]

[DOI]

Proceedings of the ECOOP 2004, 2004

A Type System for Checking Applet Isolation in Java Card.

[BibT_eX]

[DOI]

Proceedings of the Construction and Analysis of Safe, 2004

2003

Modular specification of frame properties in JML.

[BibT_eX]

[DOI]

Concurr. Comput. Pract. Exp., 2003

Formal Techniques for Java-Like Programs.

[BibT_eX]

[DOI]

Susan Eisenbach

Erik Poll

Proceedings of the Object-Oriented Technology: ECOOP 2003 Workshop Reader, 2003

2002

Modular Specification and Verification of Object-Oriented Programs

[BibT_eX]

[DOI]

Lecture Notes in Computer Science 2262, Springer, ISBN: 3-540-43167-5, 2002

2000

Formal Techniques for Java Programs.

[BibT_eX]

[DOI]

Proceedings of the Object-Oriented Technology, 2000

1999

Making Executable Interface Specifications More Expressive.

[BibT_eX]

[DOI]

Jörg Meyer

Proceedings of the JIT '99, 1999

A Programming Logic for Sequential Java.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 1999

Alias Control Is Crucial for Modular Verification of Object-Oriented Programs.

[BibT_eX]

Proceedings of the Object-Oriented Technology, ECOOP'99 Workshop Reader, 1999

Formal Techniques for Java Programs.

[BibT_eX]

[DOI]

Bart Jacobs

Proceedings of the Object-Oriented Technology, ECOOP'99 Workshop Reader, 1999

1998

Logical foundations for typed object-oriented languages.

[BibT_eX]

Proceedings of the Programming Concepts and Methods, 1998

Kapselung und Methodenbindung: Javas Designprobleme und ihre Korrektur.

[BibT_eX]

[DOI]

Proceedings of the JIT '98, 1998

1997

Formal Specification Techniques for Object-Oriented Programs.

[BibT_eX]

[DOI]