Bernhard Beckert

Proceedings of the 2nd European Workshop on Algorithmic Fairness, 2023

Static Capability-Based Security for Smart Contracts.

[BibT_eX]

[DOI]

Jonas Schiffl

Alexander Weigl

Proceedings of the IEEE International Conference on Decentralized Applications and Infrastructures, 2023

2022

Recent Developments in the Context of Online Elections and Digital Polls in Germany.

[BibT_eX]

[DOI]

Proceedings of the Sicherheit, 2022

Towards a Usable and Sustainable Deductive Verification Tool.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering, 2022

Generalized Test Tables: A Domain-Specific Specification Language for Automated Production Systems.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing - ICTAC 2022, 2022

Why Is Online Voting Still Largely a Black Box?

[BibT_eX]

[DOI]

Michael Kirsten

Melanie Volkamer

Proceedings of the Computer Security. ESORICS 2022 International Workshops, 2022

2021

Table-based formal specification approaches for control engineers - empirical studies of usability.

[BibT_eX]

[DOI]

IET Cyper-Phys. Syst.: Theory & Appl., 2021

Towards Correct Smart Contracts: A Case Study on Formal Verification of Access Control.

[BibT_eX]

[DOI]

Proceedings of the SACMAT '21: The 26th ACM Symposium on Access Control Models and Technologies, 2021

Integration of a formal specification approach into CPPS engineering workflow for machinery validation.

[BibT_eX]

[DOI]

Proceedings of the 19th IEEE International Conference on Industrial Informatics, 2021

2020

Formal Analysis of Smart Contracts: Applying the KeY System.

[BibT_eX]

[DOI]

Proceedings of the Deductive Software Verification: Future Perspectives, 2020

Integration of Static and Dynamic Analysis Techniques for Checking Noninterference.

[BibT_eX]

[DOI]

Mihai Herda

Michael Kirsten

Proceedings of the Deductive Software Verification: Future Perspectives, 2020

Nachruf Professor em. Dr. Dr. h.c. Gerhard Goos.

[BibT_eX]

[DOI]

Inform. Spektrum, 2020

Specifying Framing Conditions for Smart Contracts.

[BibT_eX]

[DOI]

Jonas Schiffl

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Applications, 2020

Modular Verification of JML Contracts Using Bounded Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles, 2020

Relational Test Tables: A Practical Specification Language for Evolution and Security.

[BibT_eX]

[DOI]

Proceedings of the FormaliSE@ICSE 2020: 8th International Conference on Formal Methods in Software Engineering, 2020

Towards classes of architectural dependability assurance for machine-learning-based systems.

[BibT_eX]

[DOI]

Proceedings of the SEAMS '20: IEEE/ACM 15th International Symposium on Software Engineering for Adaptive and Self-Managing Systems, Seoul, Republic of Korea, 29 June, 2020

2019

Understanding Counterexamples for Relational Properties with DIbugger.

[BibT_eX]

[DOI]

Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning, 2019

Using Relational Verification for Program Slicing.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering and Formal Methods - 17th International Conference, 2019

Verification-based test case generation for information-flow properties.

[BibT_eX]

[DOI]

Mihai Herda

Joachim Müssig

Proceedings of the 34th ACM/SIGAPP Symposium on Applied Computing, 2019

On the Preservation of the Trust by Regression Verification of PLC software for Cyber-Physical Systems of Systems.

[BibT_eX]

[DOI]

Proceedings of the 17th IEEE International Conference on Industrial Informatics, 2019

Smart Contracts: Application Scenarios for Deductive Program Verification.

[BibT_eX]

[DOI]

Jonas Schiffl

Proceedings of the Formal Methods. FM 2019 International Workshops, 2019

Formal Verification of Evolutionary Changes.

[BibT_eX]

[DOI]

Proceedings of the Managed Software Evolution., 2019

2018

Debugging Program Verification Proof Scripts (Tool Paper).

[BibT_eX]

[DOI]

Alexander Weigl

CoRR, 2018

Proving Equivalence Between Imperative and MapReduce Implementations Using Program Transformations.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation, 2018

Experience Report: Formal Methods in Material Science.

[BibT_eX]

[DOI]

CoRR, 2018

Applicability of generalized test tables: a case study using the manufacturing system demonstrator xPPU.

[BibT_eX]

[DOI]

Autom., 2018

Relational Equivalence Proofs Between Imperative and MapReduce Algorithms.

[BibT_eX]

[DOI]

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2018

Using Dependence Graphs to Assist Verification and Testing of Information-Flow Properties.

[BibT_eX]

[DOI]

Mihai Herda

Proceedings of the Tests and Proofs - 12th International Conference, 2018

Towards a Notion of Coverage for Incomplete Program-Correctness Proofs.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Verification, 2018

Using Theorem Provers to Increase the Precision of Dependence Analysis for Information Flow Control.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2018

Achieving delta description of the control software for an automated production system evolution.

[BibT_eX]

[DOI]

Proceedings of the 14th IEEE International Conference on Automation Science and Engineering, 2018

Trends in Relational Program Verification.

[BibT_eX]

[DOI]

Proceedings of the Principled Software Development, 2018

2017

Proving JDK's Dual Pivot Quicksort Correct.

[BibT_eX]

[DOI]

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2017

Computing Exact Loop Bounds for Bounded Program Verification.

[BibT_eX]

[DOI]

Tianhai Liu

Mana Taghdiri

Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2017

Modular Verification of Information Flow Security in Component-Based Systems.

[BibT_eX]

[DOI]

Simon Greiner

Martin Mohr

Proceedings of the Software Engineering and Formal Methods - 15th International Conference, 2017

Generalized test tables: A powerful and intuitive specification language for reactive systems.

[BibT_eX]

[DOI]

Proceedings of the 15th IEEE International Conference on Industrial Informatics, 2017

Generation of monitoring functions in production automation using test specifications.

[BibT_eX]

[DOI]

Proceedings of the 15th IEEE International Conference on Industrial Informatics, 2017

Generalised Test Tables: A Practical Specification Language for Reactive Systems.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods - 13th International Conference, 2017

SemSlice: Exploiting Relational Verification for Automatic Program Slicing.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods - 13th International Conference, 2017

An Interaction Concept for Program Verification Systems with Explicit Proof Object.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2017

2016

Dynamic Logic for Java.

[BibT_eX]

[DOI]

Benjamin Weiß

Proceedings of the Deductive Software Verification - The KeY Book, 2016

Formal Verification with KeY: A Tutorial.

[BibT_eX]

[DOI]

Proceedings of the Deductive Software Verification - The KeY Book, 2016

Automatic Margin Computation for Risk-Limiting Audits.

[BibT_eX]

[DOI]

Proceedings of the Electronic Voting - First International Joint Conference, 2016

Computing Specification-Sensitive Abstractions for Program Verification.

[BibT_eX]

[DOI]

Tianhai Liu

Proceedings of the Dependable Software Engineering: Theories, Tools, and Applications, 2016

Deductive Verification of Legacy Code.

[BibT_eX]

[DOI]

Thorsten Bormer

Daniel Grahl

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, 2016

2015

A Hybrid Approach for Proving Noninterference of Java Programs.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2015

Selected challenges of software evolution for automated production systems.

[BibT_eX]

[DOI]

Proceedings of the 13th IEEE International Conference on Industrial Informatics, 2015

Regression Verification for Programmable Logic Controller Software.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2015

Proving equivalence between control software variants for Programmable Logic Controllers.

[BibT_eX]

[DOI]

Proceedings of the 20th IEEE Conference on Emerging Technologies & Factory Automation, 2015

Regression verification for Java using a secure information flow calculus.

[BibT_eX]

[DOI]

Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs, 2015

Interactive Theorem Proving - Modelling the User in the Proof Process.

[BibT_eX]

[DOI]

Proceedings of the Workshop on Bridging the Gap between Human and Automated Reasoning, 2015

2014

Verifying voting schemes.

[BibT_eX]

[DOI]

J. Inf. Secur. Appl., 2014

Reasoning and Verification: State of the Art and Current Trends.

[BibT_eX]

[DOI]

IEEE Intell. Syst., 2014

How to Put Usability into Focus: Using Focus Groups to Evaluate the Usability of Interactive Theorem Provers.

[BibT_eX]

[DOI]

Florian Böhl

Proceedings of the Proceedings Eleventh Workshop on User Interfaces for Theorem Provers, 2014

The KeY Platform for Verification and Analysis of Java Programs.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, Tools and Experiments, 2014

A Usability Evaluation of Interactive Theorem Provers Using Focus Groups.

[BibT_eX]

[DOI]

Florian Böhl

Proceedings of the Software Engineering and Formal Methods, 2014

2013

A Dynamic Logic for deductive verification of multi-threaded programs.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2013

On the Specification and Verification of Voting Schemes.

[BibT_eX]

[DOI]

Carsten Schürmann

Proceedings of the E-Voting and Identify - 4th International Conference, 2013

A Metric for Testing Program Verification Systems.

[BibT_eX]

[DOI]

Thorsten Bormer

Markus Wagner

Proceedings of the Tests and Proofs - 7th International Conference, 2013

Information Flow in Object-Oriented Software.

[BibT_eX]

[DOI]

Proceedings of the Logic-Based Program Synthesis and Transformation, 2013

Analysing Vote Counting Algorithms via Logic - And Its Application to the CADE Election Scheme.

[BibT_eX]

[DOI]

Carsten Schürmann

Proceedings of the Automated Deduction - CADE-24, 2013

Dynamic Logic with Trace Semantics.

[BibT_eX]

[DOI]

Daniel Bruns

Proceedings of the Automated Deduction - CADE-24, 2013

2012

Lessons Learned From Microkernel Verification -- Specification is the New Bottleneck

[BibT_eX]

[DOI]

Proceedings of the Proceedings Seventh Conference on Systems Software Verification, 2012

Formal Semantics of Model Fields in Annotation-Based Specifications.

[BibT_eX]

[DOI]

Daniel Bruns

Proceedings of the KI 2012: Advances in Artificial Intelligence, 2012

Evaluating the Usability of Interactive Verification Systems.

[BibT_eX]

[DOI]

Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, 2012

2011

KeYGenU: combining verification-based and capture and replay techniques for regression unit testing.

[BibT_eX]

[DOI]

Christoph Gladisch

Amiram Yehudai

Int. J. Syst. Assur. Eng. Manag., 2011

Software Security in Virtualized Infrastructures - The Smart Meter Example.

[BibT_eX]

[DOI]

it Inf. Technol., 2011

Preface.

[BibT_eX]

[DOI]

Proceedings of the 41. Jahrestagung der Gesellschaft für Informatik, 2011

Integration of Bounded Model Checking and Deductive Verification.

[BibT_eX]

[DOI]

Proceedings of the Formal Verification of Object-Oriented Software, 2011

2010

Deductive Verification of System Software in the Verisoft XT Project.

[BibT_eX]

[DOI]

Michal Moskal

Künstliche Intell., 2010

Practical Aspects of Automated Deduction for Program Verification.

[BibT_eX]

[DOI]

Künstliche Intell., 2010

Tests and Proofs - Preface of the Special Issue.

[BibT_eX]

[DOI]

J. Autom. Reason., 2010

Deduktion: von der Theorie zur Anwendung.

[BibT_eX]

[DOI]

Franz Baader

Tobias Nipkow

Inform. Spektrum, 2010

Generating Regression Unit Tests Using a Combination of Verification and Capture & Replay.

[BibT_eX]

[DOI]

Christoph Gladisch

Amiram Yehudai

Proceedings of the Tests and Proofs - 4th International Conference, 2010

Improving the Usability of Specification Languages and Methods for Annotation-Based Verification.

[BibT_eX]

[DOI]

Thorsten Bormer

Proceedings of the Formal Methods for Components and Objects - 9th International Symposium, 2010

Mind the Gap: Formal Verification and the Common Criteria (Discussion Paper).

[BibT_eX]

[DOI]

Daniel Bruns

Proceedings of the 6th International Verification Workshop, 2010

2009

Formal Verification of a Microkernel Used in Dependable Software Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Safety, 2009

Probabilistic Models for the Verification of Human-Computer Interaction.

[BibT_eX]

[DOI]

Markus Wagner

Proceedings of the KI 2009: Advances in Artificial Intelligence, 2009

2008

Software engineering and formal methods.

[BibT_eX]

[DOI]

Bernhard K. Aichernig

Softw. Syst. Model., 2008

Title, Preface, Table of Contents.

[BibT_eX]

[DOI]

Gerwin Klein

Proceedings of the 5th International Verification Workshop in connection with IJCAR 2008, 2008

2007

Dynamic Logic.

[BibT_eX]

[DOI]

Proceedings of the Verification of Object-Oriented Software. The KeY Approach, 2007

Preface.

[BibT_eX]

[DOI]

Lawrence C. Paulson

J. Autom. Reason., 2007

White-Box Testing by Combining Deduction-Based Specification Extraction and Black-Box Testing.

[BibT_eX]

[DOI]

Christoph Gladisch

Proceedings of the Tests and Proofs - 1st International Conference, 2007

A Dynamic Logic for Deductive Verification of Concurrent Programs.

[BibT_eX]

[DOI]

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

KeY: A Formal Method for Object-Oriented Systems.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Open Object-Based Distributed Systems, 2007

The KeY system 1.0 (Deduction Component).

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2007

2006

Intelligent Systems and Formal Methods in Software Engineering.

[BibT_eX]

[DOI]

IEEE Intell. Syst., 2006

Integrating Object-Oriented Design and Deductive Verification of Software.

[BibT_eX]

[DOI]

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

A Method for Formalizing, Analyzing, and Verifying Secure User Interfaces.

[BibT_eX]

[DOI]

Gerd Beuster

Proceedings of the Formal Methods and Software Engineering, 2006

Verifying Object-Oriented Programs with KeY: A Tutorial.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Components and Objects, 5th International Symposium, 2006

Dynamic Logic with Non-rigid Functions.

[BibT_eX]

[DOI]

André Platzer

Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2005

The KeY tool.

[BibT_eX]

[DOI]

Softw. Syst. Model., 2005

Refinement and retrenchment for programming language data types.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2005

Second-Order Principles in Specification Languages for Object-Oriented Programs.

[BibT_eX]

[DOI]

Kerry Trentelman

Proceedings of the Logic for Programming, 2005

An Improved Rule for While Loops in Deductive Program Verification.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2005

2004

Proof Reuse for Deductive Program Verification.

[BibT_eX]

[DOI]

Proceedings of the 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), 2004

Software Verification with Integrated Data Type Refinement for Integer Arithmetic.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods, 4th International Conference, 2004

2003

Depth-first proof search without backtracking for free-variable clausal tableaux.

[BibT_eX]

[DOI]

J. Symb. Comput., 2003

Program Verification Using Change Information.

[BibT_eX]

[DOI]

Proceedings of the 1st International Conference on Software Engineering and Formal Methods (SEFM 2003), 2003

A Program Logic for Handling JAVA CARD's Transaction Mechanism.

[BibT_eX]

[DOI]

Wojciech Mostowski

Proceedings of the Fundamental Approaches to Software Engineering, 2003

2002

The KeY System: Integrating Object-Oriented Design and Formal Methods.

[BibT_eX]

[DOI]

Proceedings of the Fundamental Approaches to Software Engineering, 2002

2001

Free-Variable Tableaux for Propositional Modal Logics.

[BibT_eX]

[DOI]

Stud Logica, 2001

An Extension of Dynamic Logic for Modelling OCL's @pre Operator.

[BibT_eX]

[DOI]

Thomas Baar

Proceedings of the Perspectives of System Informatics, 2001

A Sequent Calculus for First-Order Dynamic Logic with Trace Modalities.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, First International Joint Conference, 2001

2000

The KeY Approach: Integrating Object Oriented Design and Formal Verification.

[BibT_eX]

[DOI]

Proceedings of the Logics in Artificial Intelligence, European Workshop, 2000

A Dynamic Logic for the Formal Verification of Java Card Programs.

[BibT_eX]

[DOI]

Proceedings of the Java on Smart Cards: Programming and Security, 2000

The 2-SAT Problem of Regular Signed CNF Formulas.

[BibT_eX]

[DOI]

Felip Manyà

Proceedings of the 30th IEEE International Symposium on Multiple-Valued Logic, 2000

1999

Proof Transformations from Search-oriented into Interaction-oriented Tableau Calculi.

[BibT_eX]

[DOI]

Gernot Stenz

Wolfgang Ahrendt

J. Univers. Comput. Sci., 1999

Proof Confluent Tableau Calculi.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 1999

Transformations between Signed and Classical Clause Logic.

[BibT_eX]

[DOI]

Felip Manyà

Proceedings of the 29th IEEE International Symposium on Multiple-Valued Logic, 1999

1998

Integration und Uniformierung von Methoden des tableaubasierten Theorembeweisens.

[BibT_eX]

[DOI]

PhD thesis, 1998

Simplification of Many-Valued Logic Formulas Using Anti-Links.

[BibT_eX]

[DOI]

Gonzalo Escalada-Imaz

J. Log. Comput., 1998

A Tableau Calculus for Quantifier-Free Set Theoretic Formulae.

[BibT_eX]

[DOI]

Ulrike Hartmer

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 1998

Fibring Semantic Tableaux.

[BibT_eX]

[DOI]

Dov M. Gabbay

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 1998

leanK 2.0.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 1998

System Description: leanK 2.0.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1998

1997

Semantic Tableaux with Equality.

[BibT_eX]

[DOI]

J. Log. Comput., 1997

Fast Subsumption Checks Using Anti-Links.

[BibT_eX]

[DOI]

J. Autom. Reason., 1997

1996

Logic Programming as a Basis for Lean Automated Deduction.

[BibT_eX]

[DOI]

J. Log. Program., 1996

Incremental Theory Reasoning Methods for Semantic Tableaux.

[BibT_eX]

[DOI]

Christian Pape

Proceedings of the Theorem Proving with Analytic Tableaux and Related Methods, 1996

The Tableau-based Theorem Prover 3TAP Version 4.0.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30, 1996

1995

leanTAP: Lean Tableau-based Deduction.

[BibT_eX]

[DOI]

J. Autom. Reason., 1995

LeanEA: A Lean Evolving Algebra Compiler.

[BibT_eX]

Proceedings of the 11. Workshop Logische Programmierung, 1995

Deduction by Combining Semantic Tableaux and Integer Programming.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 9th International Workshop, 1995

1994

Logic Programming as a Bases for Lean Deduction: Achieving Maximal Efficiency from Minimal Means.

[BibT_eX]

Proceedings of the Tenth Logic Programming Workshop, 1994

On Anti-Links.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming and Automated Reasoning, 5th International Conference, 1994

leanTAP: Lean Tableau-Based Theorem Proving (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

A Completion-Based Method for Mixed Universal and Rigid E-Unification.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

1993

The Even More Liberalized delta-Rule in Free Variable Semantic Tableaux.

[BibT_eX]

[DOI]

Proceedings of the Computational Logic and Proof Theory, Third Kurt Gödel Colloquium, 1993

1992

The Many-Valued Theorem Prover 3TAP.

[BibT_eX]

IWBS Report, 1992

Konzeption und Implementierung von Gleichheit für einen tableau-basierten Theorem-Beweiser

[BibT_eX]

IWBS Report, 1992

An Improved Method for Adding Equality to Free Variable Semantic Tableaux.

[BibT_eX]

[DOI]