Author name cluster

Bernhard Beckert

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

11 papers

2 author rows

AAAI Conference 2024 Conference Paper

An Information-Flow Perspective on Algorithmic Fairness

Samuel Teuber
Bernhard Beckert

This work presents insights gained by investigating the relationship between algorithmic fairness and the concept of secure information flow. The problem of enforcing secure information flow is well-studied in the context of information security: If secret information may "flow" through an algorithm or program in such a way that it can influence the program’s output, then that is considered insecure information flow as attackers could potentially observe (parts of) the secret. There is a strong correspondence between secure information flow and algorithmic fairness: if protected attributes such as race, gender, or age are treated as secret program inputs, then secure information flow means that these "secret" attributes cannot influence the result of a program. While most research in algorithmic fairness evaluation concentrates on studying the impact of algorithms (often treating the algorithm as a black-box), the concepts derived from information flow can be used both for the analysis of disparate treatment as well as disparate impact w.r.t. a structural causal model. In this paper, we examine the relationship between quantitative as well as qualitative information-flow properties and fairness. Moreover, based on this duality, we derive a new quantitative notion of fairness called fairness spread, which can be easily analyzed using quantitative information flow and which strongly relates to counterfactual fairness. We demonstrate that off-the-shelf tools for information-flow properties can be used in order to formally analyze a program's algorithmic fairness properties, including the new notion of fairness spread as well as established notions such as demographic parity.

PDF Details DOI

FormaliSE Conference 2024 Conference Paper

Contract Automata: A Specification Language for Mode-Based Systems

Alexander Weigl
Joshua Bachmeier
Bernhard Beckert
Mattias Ulbrich

The comprehensive, understandable and effective formal specification of complex systems is often difficult, especially for reactive and interactive systems like web services or embedded system components. In this paper, we propose contract automata, a new specification formalism for describing the expected behaviour of stateful systems. Contract automata combine two established concepts for formal system specification: contract-based specification and nondeterministic finite state automata. Contract automata restrict the effects that the operations of the specified system may have using input-output-contracts. The automaton structure of a contract automaton describes when contracts are applicable. Contract automata support the refinement and composition of reactive systems, enabling modular verification of systems assembled of multiple subsystems. In this paper, we formally define the semantics of contract automata based on a two-party game between the system under test and its environment. We define the proof obligations and present techniques to prove a refinement relationship between contract automata, the validity of system compositions, and the compliance of source code against a contract automaton. We provide a tool for the generation of the proof obligation that can be discharged with model-checkers or static program analyses. We exemplify the use of contract automata by presenting the specification and verification of an emergency brake assistant.

Details

FormaliSE Conference 2020 Conference Paper

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

Alexander Weigl
Mattias Ulbrich
Suhyun Cha
Bernhard Beckert
Birgit Vogel-Heuser

A wide range of interesting program properties are relational, i. e. , they described a relation between two program runs. Two prominent relational properties are the regression verification (proving conditional program equivalence), and non-interference (proving the absence of information flow). The verification of relational properties is hardly accessible to engineers due to the lack of appropriate specification languages for relational properties. In previous work, we introduced the concept of generalized test tables: a table-based specification language, which allows the tight temporal specification of functional (nonrelational) properties for reactive systems. We introduce relational test tables-an extension of generalized test tables for the specification of relational properties. Relational test tables support specification of k-safety properties (a super set of relational properties) between $k\geq 2$ program runs. We show the applicability of relational test tables by specifying and verifying change scenarios and information flow of reactive systems. We provide an implementation of the verification pipeline for programs following the IEC 61131-3 coding standard under http://github.com/VerifAPS/verifaps-lib.CCS CONCEPTS• Software and its engineering $\rightarrow$ Software verification; Model checking; • General and reference $\rightarrow$ Verification; • Security and privacy $\rightarrow$ Software security engineering.

Details

IS Journal 2014 Journal Article

Reasoning and Verification: State of the Art and Current Trends

Bernhard Beckert
Reiner Hähnle

In this article, the authors give an overview of tool-based verification of hardware and software systems and discuss the relation between verification and logical reasoning. Here, "verification"' refers to reasoning-based methods to establish dependability. This isn't restricted to proofs of functional correctness; it also includes other scenarios such as test generation and bug finding. The authors describe the main verification scenarios and methods that are in use today and the extent to which they depend on logical reasoning. From this discussion, they distill current trends and new opportunities for the interaction between verification and reasoning.

Details DOI

LOPSTR Conference 2013 Conference Paper

Information Flow in Object-Oriented Software

Bernhard Beckert
Daniel Bruns
Vladimir Klebanov
Christoph Scheben
Peter H. Schmitt
Mattias Ulbrich

Abstract This paper contributes to the investigation of object-sensitive information flow properties for sequential Java, i. e. , properties that take into account information leakage through objects, as opposed to primitive values. We present two improvements to a popular object-sensitive non-interference property. Both reduce the burden on analysis and monitoring tools. We present a formalization of this property in a program logic – JavaDL in our case – which allows using an existing tool without requiring program modification. The third contribution is a novel fine-grained specification methodology. In our approach, arbitrary JavaDL terms (read ‘side-effect-free Java expressions’) may be assigned a security level – in contrast to security labels being attached to fields and variables only.

Details

IS Journal 2006 Journal Article

Intelligent Systems and Formal Methods in Software Engineering

Bernhard Beckert
Tony Hoare
Reiner Hahnle
Douglas Smith
Cordell Green
Silvio Ranise
Cesare Tinelli
Thomas Ball

Over the last few years, technologies for the formal description, construction, analysis, and validation of software - based mostly on logics and formal reasoning - have matured. We can expect them to complement and partly replace traditional software engineering methods in the future. Formal methods in software engineering are an increasingly important application area for intelligent systems. The field has outgrown the area of academic case studies, and industry is showing serious interest. We convincingly argue that we've reached the point where we can solve the problem of how to formally verify industrial-scale software. We propose program verification as a computer science Grand Challenge. Deductive software verification is a core technology of formal methods. We describe recent dramatic changes in the way it's perceived and used. Another important base technique of formal methods, besides software verification, is synthesizing software that's correct by construction because it's formally derived from its specification. We discuss recent developments and trends in this area. Surprisingly efficient decision procedures for the satisfiability modulo theories problem have recently emerged. We explain these techniques and why they're important for all formal-methods tools. We look at formal methods from an industry perspective. We explain the success of Microsoft Research's SLAM project, which has developed a verification tool for device drivers

Details DOI

LPAR Conference 2005 Conference Paper

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

Bernhard Beckert
Kerry Trentelman

Abstract Within the setting of object-oriented program specification and verification, pointers and object references can be considered as relations between the elements of a data structure. When we specify properties of these data structures, we often describe properties of relations. Hence it is important to be able to talk about relations and their properties when specifying object-oriented programs or programs with pointers. Many interesting properties of relations such as transitive closure, finiteness, and generatedness are not expressible in first-order logic (FOL); hence neither are they expressible in first-order fragments of specification languages. In this paper we give an overview of the different ways such properties can be expressed in various logics, with a particular emphasis on extensions of FOL, i. e. transitive closure logic, fixed-point logic, and first-order dynamic logic. Within the paper we also discuss which of these extensions already are – or in fact should be – implemented within specification languages. We feel that such a discussion is necessary since it is often the case that when an extension of FOL is implemented within a specification language it is done so in an ad hoc manner or the underpinning logical concepts are not well documented.

Details

JELIA Conference 2000 Invited Paper

The KeY Approach: Integrating Object Oriented Design and Formal Verification

Wolfgang Ahrendt
Thomas Baar
Bernhard Beckert
Martin Giese
Elmar Habermalz
Reiner Hähnle
Wolfram Menzel
Peter H. Schmitt

Abstract This paper reports on the ongoing KeY project aimed at bridging the gap between (a) object-oriented software engineering methods and tools and (b) deductive verification. A distinctive feature of our approach is the use of a commercial CASE tool enhanced with functionality for formal specification and deductive verification.

Details

CSL Conference 1996 Conference Paper

Deduction by Combining Semantic Tableaux and Integer Programming

Bernhard Beckert
Reiner Hähnle

Abstract In this paper we propose to extend the current capabilities of automated reasoning systems by making use of techniques from integer programming. We describe the architecture of an automated reasoning system based on a Herbrand procedure (enumeration of formula instances) on clauses. The input are arbitrary sentences of first-order logic. The translation into clauses is done incrementally and is controlled by a semantic tableau procedure using unification. This amounts to an incremental polynomial CNF transformation which at the same time encodes part of the tableau structure and, therefore, tableau-specific refinements that reduce the search space. Checking propositional unsatisfiability of the resulting sequence of clauses can either be done with a symbolic inference system such as the Davis-Putnam procedure or it can be done using integer programming. If the latter is used a number of advantages become apparent.

Details

CSL Conference 1996 Conference Paper

leanEA: A Lean Evolving Algebra Compiler

Bernhard Beckert
Joachim Posegga

Abstract The Prolog program “term_expansion((define C as A with B), (C=>A: -B, !)). term-expansion((transition E if C then D), ((transition E): -C, !, B, A, (transition _))): -rearrange(D, B, A). rearrange((E, F), (C, D), (A, B)): -rearrange(E, C, B), rearrange(F, D, A). rearrange(F: =G, ([G]=>*[E], F=. [C¦D], D=>*B, A=. [C¦B]), asserta(A=>E)). [G¦H]=>*[E¦F]: -(G=>E; G=. [C¦D], D=>*B, A=. [C¦B], A=>E), !, H=>*F. []=>*[]. A=? B: - [A, B]=>*[D, C], D==C. ” implements an efficient and flexible simulator for evolving algebra specifications.

Details

LPAR Conference 1994 Conference Paper

On Anti-Links

Bernhard Beckert
Reiner Hähnle
Anavai Ramesh
Neil V. Murray

Abstract The concept of anti-link is defined, and useful equivalence-preserving operations on propositional formulas based on anti-links are introduced. These operations eliminate a potentially large number of subsumed paths in a negation normal form formula. The operations have linear time complexity in the size of that part of the formula containing the anti-link. These operations are useful for prime implicant/implicate algorithms because most of the computational effort in such algorithms is spent on subsumption checks.

Details