Viper: A verification infrastructure for permission-based reasoning P Müller, M Schwerhoff, AJ Summers Verification, Model Checking, and Abstract Interpretation: 17th …, 2016 | 539 | 2016 |
Advancing Automated, Permission-Based Program Verification Using Symbolic Execution M Schwerhoff ETH Zurich, 2016 | 56 | 2016 |
Automatic verification of iterated separating conjunctions using symbolic execution P Müller, M Schwerhoff, AJ Summers Computer Aided Verification: 28th International Conference, CAV 2016 …, 2016 | 56 | 2016 |
Lightweight support for magic wands in an automatic verifier M Schwerhoff, AJ Summers 29th European Conference on Object-Oriented Programming (ECOOP 2015), 2015 | 47 | 2015 |
Viper: A verification infrastructure for permission-based reasoning U Juhasz, IT Kassios, M Novacek, M Schwerhoff, AJ Summers | 44 | 2014 |
Comparing verification condition generation with symbolic execution: an experience report IT Kassios, P Müller, M Schwerhoff Verified Software: Theories, Tools, Experiments: 4th International …, 2012 | 25 | 2012 |
Concise outlines for a complex logic: a proof outline checker for TaDA FA Wolf, M Schwerhoff, P Müller Formal Methods: 24th International Symposium, FM 2021, Virtual Event …, 2021 | 24 | 2021 |
Symbolic execution for Chalice M Schwerhoff Eidgenössische Technische Hochschule Zürich, Departement of Computer Science …, 2011 | 16 | 2011 |
Constraint semantics for abstract read permissions JT Boyland, P Müller, M Schwerhoff, AJ Summers Proceedings of 16th Workshop on Formal Techniques for Java-like Programs, 1-6, 2014 | 11 | 2014 |
A generic methodology for the modular verification of security protocol implementations L Arquint, M Schwerhoff, V Mehta, P Müller Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications …, 2023 | 9 | 2023 |
Verifying scala traits M Schwerhoff Semester Report, Swiss Federal Institute of Technology Zurich (ETH), 2010 | 5 | 2010 |
Concise outlines for a complex logic: a proof outline checker for TaDA (full paper) FA Wolf, M Schwerhoff, P Müller arXiv preprint arXiv:2010.07080, 2020 | 4 | 2020 |
Debugging Symbolic Execution I Colombo, M Schwerhoff, P Müller Master's Thesis, ETH Zurich, 2012 | 4 | 2012 |
Verification Algorithms for Automated Separation Logic Verifiers M Eilers, M Schwerhoff, P Müller International Conference on Computer Aided Verification, 362-386, 2024 | 2 | 2024 |
Profiling Symbolic Execution L Arquint ETH Zurich, 2019 | 1 | 2019 |
Recording symbolic executions A Buob, M Schwerhoff, P Müller | 1 | 2015 |
Explaining Unsatisfiability Proofs through Examples P Strebel, M Schwerhoff | | 2021 |
Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA P Müller, FA Wolf, M Schwerhoff arXiv, 2010.07080, 2020 | | 2020 |
Adding Generalized Magic Wand Support to a Verification Condition Generation Based Verifier A Gamal, AJ Summers, M Schwerhoff | | 2018 |
Lightweight Support for Magic Wands in an Automatic Verifier (Artifact). M Schwerhoff, AJ Summers Dagstuhl Artifacts Ser. 1 (1), 10:1-10:2, 2015 | | 2015 |