VSL 2014: VIENNA SUMMER OF LOGIC 2014
VERIFY ON WEDNESDAY, JULY 23RD, 2014

View: session overviewtalk overviewside by side with other conferences

08:45-10:15 Session 159F: Invited Talk and Contributed Talk (joint with ARW-DT and WING)
Location: FH, Hörsaal 3
08:45
Chasing the Perfect Specification
09:45
Typed First-Order Logic
SPEAKER: Peter Schmitt

ABSTRACT. This paper contributes to the theory of typed first-order logic. We present a sound and complete axiomatization lifting restriction imposed by previous results. We resolve an issue with modular reasoning. As a third contribution this paper provides complete axiomatizations for the type predicates $instance_{T}$, $exactInstance_{T}$, and functions $cast_{T}$ indispensible for reasoning about object-oriented programming languges.

10:15-10:45Coffee Break
10:45-12:15 Session 166L: Contributed Talks (joint with ARW-DT and WING)
Location: FH, Hörsaal 3
10:45
Reasoning About Vote Counting Schemes Using Light-weight and Heavy-weight Methods
SPEAKER: unknown

ABSTRACT. We compare and contrast our experiences in specifying, implementing and verifying the monotonicity property of a simple plurality voting scheme using modern light-weight and heavy-weight verification tools.

11:15
Introducing a Sound Deductive Compilation Approach
SPEAKER: unknown

ABSTRACT. Compiler verification is difficult and expensive. Instead of formally verifying a compiler, we introduce a sound deductive compilation approach, whereby verified bytecode is generated based on symbolic execution of source code embedded in a program logic. The generated bytecode is weakly bisimilar to the original source code relative to a set of observable locations. The framework is instantiated for Java source and bytecode. The compilation process is fully automatic and first-order solvers are employed for bytecode optimization.

11:45
Verifying safety properties of Artificial General Intelligence: The ultimate safety-critical system?

ABSTRACT. In this paper, we discuss the challenge of verifying a system which does not exist today, but may be of the utmost importance in the future: an Artificial General Intelligence (AGI) as smart or smarter than human beings, and capable of improving itself further.

A self-improving AGI with the potential to become more powerful than any human would be a system we'd need to design for safety from the ground up. We argue that this will lead to foreseeable technical difficulties which we can and should start working on today, despite the fact that we do not yet know how to build an AGI. In this paper, we focus on one particular such difficulty: We could require an AGI to exhibit a formal proof that each of its actions and self-rewrites satisfy a certain safety property, and otherwise switch to a baseline controller (a variation on the well-known simplex architecture), but straight-forward ways of implementing this for a self-rewriting AGI run into problems related to Gödel's incompleteness theorems. We review several potential solutions to this problem and discuss reasons to think that it is likely to be an issue for a wide variety of potential approaches to constructing a safe self-improving AGI.

12:15-13:15 Session 171B: Verification: Contributed Talks (joint with ARW-DT and WING)
Location: FH, Hörsaal 3
12:15
Reasoning about Auctions
SPEAKER: unknown

ABSTRACT. In the ForMaRE project formal mathematical reasoning is applied to economics. After an initial exploratory phase, it focused on auction theory and has produced, as its first results, formalized theorems and certified executable code.

12:45
Automating Regression Verification

ABSTRACT. Regression verification is an approach to prevent regressions in software development using formal verification. The goal is to prove that two versions of a program behave equally or differ in a specified way. We worked on an approach for regression verification, extending Strichman and Godlin's work by relational equivalence and two ways of using counterexamples.

13:00-14:30Lunch Break
16:00-16:30Coffee Break