diff --git a/_layouts/programme.html b/_layouts/programme.html index c595bf2..1d16acf 100644 --- a/_layouts/programme.html +++ b/_layouts/programme.html @@ -16,24 +16,25 @@ {%- endmacro %} {% macro session(name, chair, slots) -%} -
+ Session: {{name}} ∣ Chair: {{user(chair)}} -
+
{%for s in slots%} {{talk(s)}}{%endfor%} {%- endmacro %} {% macro talk(slotId) -%} {% if slotId in bySlot %} {% set t = bySlot[slotId] %} -
+

- + {{ t.meta.title }} + {{ t.meta.length }} min.
{{user(t.meta.author)}} -

+

{% else %} @@ -44,206 +45,174 @@ {% block content %} -

Programme

+

Prelimniary Programme

+

more like a draft than final

-{{content|safe}} - -
- -

- - Day 0 -

- -
+

Day 0 - Monday, 29th July

- - + + - + - + - + - + - +
#Topic#Topic
13:00--17:0013:00 – 17:00 {{talk(999)}}
17:00--18:0017:00 –18:00 Registration
18:00--19:0018:00 –19:00 Dinner at Haus der Kirche
19:00--Getting Together19:00 –Getting Together
20:00--21:00Meeting of the Programme Board20:00 –21:00Meeting of the Programme Board
-
-
- -
- -

- - Day 1 -

- -
+ +

Day 1 – Tuesday, 30th July

- - + + - + - + - + - - - + + + + + + + + + - + - - - + + + + + + + + + - + - + - + - +
#Topic#Topic
08:45--09:0008:45 –09:00 {{ talk(10) }}
09:00--10:3009:00 –10:30 - {{ session("#1", "X", [11,12]) }} + {{ session("Probabilism", "X", [11,12,123]) }}
10:30--11:0010:30 –11:00 Coffee
11:00 -- 12:30 - {{ session("#2", "X", [13,14,15]) }} -
11:00 – 12:30 {{ session("#6a", "X", [113,114,115]) }}
11:00 – 12:30 {{ session("#6b", "X", [213,214,215]) }}
12:30 -- 14:0012:30 – 14:00 Lunch
14:00 -- 15:30 - {{ session("#3", "X", [16,17,18]) }} -
14:00 – 15:30 {{ session("#7a", "X", [116,117,118]) }}
14:00 – 15:30 {{ session("#7b", "X", [216,217,218]) }}
15:30 -- 16:0015:30 – 16:00 Coffee
16:00 -- 18:0016:00 – 17:30 - {{ session("#4", "X", [19,110,111,112]) }} + {{ session("Voting, Social-Choice", "Michael Kirsten", [19,191,192,193]) }}
18:00 -- 19:0018:00 – 19:00 Dinner at HdK
-
-
- -
- -

- - Day 2 -

- -
+ + +

Day 2 – Wednesday, 31th July

+ - - + + - + - + - - - - - - - - + + + - + - - - - - - - - + + + - + - - - + + + - - - - - +
#Topic#Topic
09:00--10:3009:00 –10:30 - {{ session("#5", "X", [20,21]) }} + {{ session("Formal Methods for CPS", "X", [20,21,22]) }}
10:30--11:0010:30 –11:00 Coffee
11:00 -- 12:30 {{ session("#6a", "X", [201,202,203]) }}
11:00 -- 12:30 {{ session("#6b", "X", [210,211,212]) }}
11:00 – 12:30 + {{ session("#2", "X", [13,14,15]) }} +
12:30 -- 14:0012:30 – 14:00 Lunch
14:00 -- 15:30 {{ session("#7a", "X", [204,205,206]) }}
14:00 -- 15:30 {{ session("#7b", "X", [214,215,216]) }}
14:00 – 15:30{{ session("#3", "X", [207,208,209]) }}
15:30 -- 16:0015:30 – 16:00 Coffee
16:00 -- 18:00 {{ session("#7a", "X", [207,208,209,2010]) }}
16:00 – 18:00 + {{ session("Intersymbolic AI", "X", [16,17,18,199]) }} +
16:00 -- 18:00{{ session("#7b", "X", [217,218,219,2110]) }}
18:30 --18:30 – Dinner outside
-
-
+ +

Day 3 – Thursday, 1st August

-
- -

- - Day 3 -

- -
+
@@ -251,31 +220,29 @@

- + - + - + - +
#
09:00--10:3009:00 –10:30 {{ session("#8", "X", [30,31]) }}
10:30--11:0010:30 –11:00 Coffee
11:00 -- 12:3011:00 – 12:30 - {{ session("#8", "X", [32,33,34,35]) }} + {{ session("#8", "X", [32,33,34,35,36]) }}
12:30 -- 14:0012:30 – 14:00 Lunch
-
-

Talks

@@ -291,10 +258,9 @@

{{t.meta.title}}

{{user(t.meta.author)}}

- -

+

{{t.content | safe }} -

+
{% endfor %} diff --git a/config.yml b/config.yml index 6a79136..100da23 100644 --- a/config.yml +++ b/config.yml @@ -4,6 +4,145 @@ persons: "Martin Fränzle": link: "https://uol.de/socps/personen/prof-dr-martin-fraenzle" image: "https://uol.de/f/2/_processed_/a/8/csm_2017_11_Martin_Fraenzle_2_742ee467bb.jpg" - "X": - link: "#" - image: "#" + + "Noah Abou El Wafa": + mail: "noah.abouelwafa@kit.edu" + link: "" + "Wolfgang Ahrendt": + mail: "ahrendt@chalmers.se" + link: "" + "Thomas Baar": + mail: "thomas.baar@htw-berlin.de" + link: "" + "Joshua Bachmeier": + mail: "j.bachmeier@fzi.de" + link: "" + "Bernhard Beckert": + mail: "beckert@kit.edu" + link: "https://formal.iti.kit.edu/beckert" + "Tabea Bordis": + mail: "tabea.bordis@kit.edu" + link: "" + "Marvin Brieger": + mail: "marvin.brieger@sosy.ifi.lmu.de" + link: "" + "Richard Bubel": + mail: "bubel@cs.tu-darmstadt.de" + link: "" + "Julia Butte": + mail: "uegqr@student.kit.edu" + link: "" + "Stijn de Gouw": + mail: "sdg@ou.nl" + link: "" + "Daniel Drodt": + mail: "daniel.drodt@tu-darmstadt.de" + link: "" + "Henriette Färber": + mail: "henriette.faerber@student.kit.edu" + link: "" + "George Granberry": + mail: "george.granberry@gmail.com" + link: "" + "Lukas Grätz": + mail: "lukas.graetz@tu-darmstadt.de" + link: "" + "Reiner Hähnle": + mail: "reiner.haehnle@tu-darmstadt.de" + link: "" + "Jonathan Hellwig": + mail: "jonathan.hellwig@kit.edu" + link: "" + "Asmae Heydari Tabar": + mail: "asmae.heydari-tabar@kit.edu" + link: "" + "Carlos Ignacio Isasa Martin": + mail: "cisasa@ece.au.dk" + link: "" + "Aditi Kabra": + mail: "akabra@andrew.cmu.edu" + link: "" + "Eduard Kamburjan": + mail: "eduard@ifi.uio.no" + link: "" + "Philipp Kern": + mail: "philipp.kern@kit.edu" + link: "https://formal.iti.kit.edu/kern" + "Michael Kirsten": + mail: "kirsten@kit.edu" + link: "https://formal.iti.kit.edu/kirsten" + "Jonas Klamroth": + mail: "klamroth@fzi.de" + link: "" + "Maximilian Kodetzki": + mail: "maximilian.kodetzki@kit.edu" + link: "" + "Florian Lanzinger": + mail: "lanzinger@kit.edu" + link: "https://formal.iti.kit.edu/lanzinger" + "Jonathan Laurent": + mail: "jonathan.laurent@kit.edu" + link: "" + "Debasmita Lohar": + mail: "debasmita.lohar@kit.edu" + link: "https://formal.iti.kit.edu/lohar" + "Joscha Mennicken": + mail: "uzuue@student.kit.edu" + link: "" + "Wojciech Mostowski": + mail: "wojciech.mostowski@hh.se" + link: "" + "Joel Nyholm": + mail: "joel.nyholm@hh.se" + link: "" + "Romain Pascual": + mail: "romain.pascual@kit.edu" + link: "https://formal.iti.kit.edu/pascual" + "Wolfram Pfeifer": + mail: "wolfram.pfeifer@kit.edu" + link: "https://formal.iti.kit.edu/pfeifer" + "Andre Platzer": + mail: "platzer@kit.edu" + link: "https://symbolaris.org" + "Enguerrand Prebet": + mail: "enguerrand.prebet@kit.edu" + link: "" + "Long Qian": + mail: "longq@andrew.cmu.edu" + link: "" + "Marco Scaletta": + mail: "scaletta@cs.tu-darmstadt.de" + link: "" + "Ina Schaefer": + mail: "ina.schaefer@kit.edu" + link: "" + "Jonas Schiffl": + mail: "jonas.schiffl@kit.edu" + link: "https://formal.iti.kit.edu/schiffl" + "Peter Schmitt": + mail: "peter.schmitt@kit.edu" + link: "" + "Anna Schmitt": + mail: "Anna.Schmitt@tu-darmstadt.de" + link: "" + "Guilherme Silva": + mail: "alvares@chalmers.se" + link: "" + "Yong Kiam Tan": + mail: "tanyongkiam@gmail.com" + link: "" + "Samuel Teuber": + mail: "teuber@kit.edu" + link: "https://formal.iti.kit.edu/teuber" + "Shmuel Tyszberowicz": + mail: "tyshbe@tau.ac.il" + link: "" + "Mattias Ulbrich": + mail: "ulbrich@kit.edu" + link: "https://formal.iti.kit.edu/ulbrich" + "Adele Veschetti": + mail: "adele.veschetti@tu-darmstadt.de" + link: "" + "Alexander Weigl": + mail: "weigl@kit.edu" + link: "https://formal.iti.kit.edu/weigl" diff --git a/render.py b/render.py index fd0504b..27b50fe 100755 --- a/render.py +++ b/render.py @@ -74,7 +74,10 @@ def render_program(): for fn in Path("talks/").rglob("*.md"): t = _read(fn) talks.append(t) - bySlot[t.meta['slot']] = t + try: + bySlot[t.meta['slot']] = t + except: + print(f"No slot given in {fn}") with open(PUBLIC/"programme.html", 'w') as fh: fh.write(template.render(content=p.content, page=p.meta, talks=talks, bySlot=bySlot, site=SITE)) diff --git a/talks/abouelwafa.md b/talks/abouelwafa.md new file mode 100644 index 0000000..88936de --- /dev/null +++ b/talks/abouelwafa.md @@ -0,0 +1,9 @@ +--- +author: "Noah Abou El Wafa" +kind: "Regular Talk (20 min. + 10 min.)" +track: "KeYmaera Track" +title: "tbd" +slot: 216 +length: 30 +--- + diff --git a/talks/akabra.md b/talks/akabra.md new file mode 100644 index 0000000..51244fb --- /dev/null +++ b/talks/akabra.md @@ -0,0 +1,9 @@ +--- +author: "Aditi Akabra" +kind: "Short Talk (10 min. + 5 min.)" +track: "KeYmaera Track" +title: "Control Envelope Synthesis in KeYmaera X" +slot: 214 +length: 30 +--- + diff --git a/talks/alvares.md b/talks/alvares.md new file mode 100644 index 0000000..b502cbf --- /dev/null +++ b/talks/alvares.md @@ -0,0 +1,12 @@ +--- +author: "Guilherme Silva" +kind: "Regular Talk (20 min. + 10 min.)" +track: "KeY-only Track" +title: "Modeling Solidity data types in SolidiKeY" +slot: 32 +length: 30 +--- + +Solidity, the main programming language for smart contracts in cryptocurrencies, is being formalized in KeY. +One of the main challenges is to modeling data types to it. +These data types are different from Java in some interesting ways. diff --git a/talks/anna.schmitt.md b/talks/anna.schmitt.md new file mode 100644 index 0000000..7142162 --- /dev/null +++ b/talks/anna.schmitt.md @@ -0,0 +1,10 @@ +--- +author: "Anna Schmitt" +kind: "Short Talk (10 min. + 5 min.)" +track: "Common Track" +title: "tbd" +length: 15 +slot: 12 +--- + +Keywords: Probabilistic Process Calculi, Encodings, Quantum Based Systems diff --git a/talks/beyer.md b/talks/beyer.md new file mode 100644 index 0000000..39dbc45 --- /dev/null +++ b/talks/beyer.md @@ -0,0 +1,10 @@ +--- +author: "Dirk Beyer" +kind: "Invited Talk" +track: "Common Track" +title: "tbd" +slot: 207 +length: 60 +--- + +Stipula is an executable language that formalizes the operational semantics of legal contracts. It combines aspects from state automata, time, asynchronous and imperative programming. We sketch how a large class of Stipula programs can be modeled and formally verified in KeY. This is joint work with Cosimo Laneve (U Bologna) and Adele Veschetti. diff --git a/talks/blanchett.md b/talks/blanchett.md new file mode 100644 index 0000000..d89540d --- /dev/null +++ b/talks/blanchett.md @@ -0,0 +1,8 @@ +--- +author: Jasmin Blanchett +kind: "Invited Talk (60 min.)" +track: "Common Track" +title: "tbd" +slot: 30 +length: 60 +--- diff --git a/talks/bordis.md b/talks/bordis.md new file mode 100644 index 0000000..68f9bdf --- /dev/null +++ b/talks/bordis.md @@ -0,0 +1,12 @@ +--- +author: "Tabea Bordis" +kind: "Either Regular or Short. Whatever fits best into the program." +track: "Common Track" +title: "Free Facts: An Alternative to Inefficient Axioms in Dafny" +slot: 13 +length: 30 +--- + +Formal software verification relies on properties of functions and built-in operators. Unless these properties are handled directly by decision procedures, an automated verifier includes them in verification conditions by supplying them as universally quantified axioms or theorems. The use of quantifiers sometimes leads to bad performance, especially if automation causes the quantifiers to be instantiated many times. + +In this presentation, I will talk about free facts as an alternative to some axioms. A free fact is a pre-instantiated axiom that is generated alongside the formulas in a verification condition that can benefit from the facts. Replacing an axiom with free facts thus reduces the number of quantifiers in verification conditions. Free facts are statically triggered by syntactic occurrences of certain patterns in the proof terms. This is less powerful than the dynamically triggered patterns used during proof construction. However, we found that free facts perform well in practice. diff --git a/talks/bubel.md b/talks/bubel.md new file mode 100644 index 0000000..c1362ad --- /dev/null +++ b/talks/bubel.md @@ -0,0 +1,10 @@ +--- +author: "Richard Bubel" +kind: "Regular Talk (20 min. + 10 min.)" +track: "KeY-only Track" +title: "Verification of the Norway Election Algorithm" +slot: 191 +length: 30 +--- + +We present the verification of the Norway Election Algorithm using the KeY Tool. We report on the approach and experiences. diff --git a/talks/buchholz.md b/talks/buchholz.md new file mode 100644 index 0000000..ec1a205 --- /dev/null +++ b/talks/buchholz.md @@ -0,0 +1,18 @@ +--- +author: "Nils Buchholz" +kind: "Regular Talk (20 min. + 10 min.)" +track: "KeY-only Track" +title: "Transferring proof obligations from KeY to Isabelle/HOL" +slot: 31 +length: 15/30 +--- + +*Can be reduced to short talk if necessary* + +Guarantees of correctness of programs are becoming more and more important nowadays. KeY is one tool, which can be used to prove the formal correctness of Java programs. It uses syntactic rewriting rules, called taclets, to successively simplify proofs. These taclet rules can be applied by an automated proving mode in KeY. Because the automation can be insufficient for closing some proofs and because proofs can contain thousands of rule applications, it is desirable to provide stronger automated tools to the user. One such tool is the Satisfiablity Modulo Theories (SMT) translation of KeY, which allows the use of SMT provers to close proofs. The SMT translation also lacks the required rules or proving strength for some proofs. It is thus still desirable to improve the already present automated toolset of KeY users. + +This work designs a translation of KeY proofs to the higher-order logic prover Isabelle/HOL. In addition to designing this translation this work also shows that the translation can be automated and integrated within KeY by implementing it as a GUI-Extension of KeY. + +This work tests the developed Isabelle translation on over 2 400 example proof obligations of KeY. In doing so the Isabelle translation has been found to offer some advantages over the SMT translation and the KeY automation. Although the Isabelle translation does not manage to close all proofs the KeY automation or SMT translation could close, it is able to close proofs, which the KeY automation or the SMT translation could not close. + +Thus the Isabelle translation expands the KeY user’s automated toolset in a meaningful way, while also building a foundation for using Isabelle in ways outside automated proof solving in KeY. diff --git a/talks/cisasa.md b/talks/cisasa.md new file mode 100644 index 0000000..cef9542 --- /dev/null +++ b/talks/cisasa.md @@ -0,0 +1,10 @@ +--- +author: "Carlos Ignacio Isasa Martin" +kind: "Regular Talk (20 min. + 10 min.)" +track: "KeYmaera Track" +title: "Formal Verification of 2-Element Lumped-Capacitance Model" +slot: 217 +length: 30 +--- + +We show a verified controller that regulates a heat exchange system. diff --git a/talks/closing.md b/talks/closing.md index 0e2a7ae..2b650de 100644 --- a/talks/closing.md +++ b/talks/closing.md @@ -4,7 +4,8 @@ author: - "Bernhard Beckert" - "Reiner Hähnle" title: "Closing Cerenomy" -slot: 35 +slot: 36 +length: 10 --- Closing cerenomy diff --git a/talks/degouw.md b/talks/degouw.md new file mode 100644 index 0000000..0d2ea44 --- /dev/null +++ b/talks/degouw.md @@ -0,0 +1,10 @@ +--- +author: "Stijn de Gouw" +kind: "Regular Talk (20 min. + 10 min.)" +track: "Common Track, KeY-only Track" +title: "Analyzing OpenJDK's BitSet" +slot: 117 +length: 30 +--- + +We analyse OpenJDK's BitSet class with a combination of formal specification, testing and preliminary verification. The BitSet class represents a vector of bits that grows as required. During our analysis, we uncovered a number of bugs. We propose and compare various solutions, supported by our formal specification. Until a solution is chosen for the discovered problems, the source code is not (sufficiently) fixed to allow full mechanical verification in KeY of the class. But we do show initial steps taken towards verification, discuss our experience and identify necessary extensions (particularly for bitwise operations) required to make a complete proof possible once the source code is stable. diff --git a/talks/drodt.md b/talks/drodt.md new file mode 100644 index 0000000..7f58f1f --- /dev/null +++ b/talks/drodt.md @@ -0,0 +1,10 @@ +--- +author: "Daniel Drodt" +kind: "Regular Talk (20 min. + 10 min.)" +track: "Common Track, KeY-only Track" +title: "Rusty KeY" +length: 30 +slot: 113 +--- + +TBD diff --git "a/talks/fr\303\244nzle.md" "b/talks/fr\303\244nzle.md" index 0554aa2..8cdee3b 100644 --- "a/talks/fr\303\244nzle.md" +++ "b/talks/fr\303\244nzle.md" @@ -1,8 +1,9 @@ --- author: "Martin Fränzle" title: "Why does so much CPS design go on without much formal methods? A plea for developing verification theories bridging exhaustive and statistical correctness arguments, stochasticity, and open systems" -slot: 2 +slot: 20 type: invited +length: 45 --- Cyber-physical systems are systems whose design calls for a meet of various engineering disciplines, all with their own mathematical as well as empirical modelling and analysis techniques. Sadly, even after more than half of a century of scientific interest in the control of hybrid discrete-continuous systems and after more than three decades of dedicated conferences and collaborative research agendas unifying theories from dynamical systems, control, and computer science, these methods still do not meet as seamlessly as we in the formal methods community tend to claim. While we, as a formal methods community together with our peers from control theory, have made tremendous progress in the formal verification of hybrid-state dynamical systems and thereby of cyber-physical systems, industrial adoption of these methods remains meagre. Our perception in the FM community tends to be that this is due to still limited usability and scalability of our tools, and thus to be solved eventually by their further development. I will in my talk argue that the problem actually lies much deeper: all tools and theories around do only cover fragmentary aspects of a CPS's correctness argument, and they unfortunately don't interface well to together provide an overarching argument. Not only does the impossibility of building 100% correct cyber-physical systems, which is induced by the inherent uncertainties in sensing and component behaviour, force us into quantitative safety arguments, but we then even have to provide such quantitative arguments for open systems, where input distributions may be vague and instationary. And industrial supplier and subcontractor structures also enforce compositional reasoning, asking for inferences combining rigorous verification certificates for one component with statistical evidence from (virtual or physical) experiments for the other. Can we establish compositional verification theories reconciling rigorous, exhaustive and statistical correctness arguments, stochasticity, and open systems? Maybe, and he talk will show some ideas of setting up such a framework (joined work with Pauline Blohm (U Münster), Paula Herber (U Münster), Paul Kröger (U Oldenburg) und Anne Remke (U Münster)). Can we do without such? Maybe not, unless we can live with limited impact. diff --git a/talks/graetz.md b/talks/graetz.md new file mode 100644 index 0000000..c476894 --- /dev/null +++ b/talks/graetz.md @@ -0,0 +1,9 @@ +--- +author: "lukas.graetz@tu-darmstadt.de" +kind: "Regular Talk (20 min. + 10 min.)" +track: "Common Track" +title: "Single Path Verification for Validation or Debugging" +slot: 14 +length: 30 +--- + diff --git a/talks/granberry.md b/talks/granberry.md new file mode 100644 index 0000000..1d482ad --- /dev/null +++ b/talks/granberry.md @@ -0,0 +1,10 @@ +--- +author: "George Granberry" +kind: "Regular Talk (20 min. + 10 min.)" +track: "KeY-only Track" +title: "Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods" +length: 30 +slot: 17 +--- + +We investigate how combinations of Large Language Models (LLMs) and symbolic analyses can be used to synthesise specifications of C programs. The LLM prompts are augmented with outputs from two formal methods tools in the Frama-C ecosystem, Pathcrawler and EVA, to produce C program annotations in the specification language ACSL. We demonstrate how the addition of symbolic analysis to the workflow impacts the quality of annotations: information about input/output examples from Pathcrawler produce more context-aware annotations, while the inclusion of EVA reports yields annotations more attuned to runtime errors. In addition, we show that the method infers rather the programs intent than its behaviour, by generating specifications for buggy programs and observing robustness of the result against bugs. diff --git a/talks/haehnle.md b/talks/haehnle.md new file mode 100644 index 0000000..c7dca89 --- /dev/null +++ b/talks/haehnle.md @@ -0,0 +1,10 @@ +--- +author: "Reiner Hähnle" +kind: "Regular Talk (20 min. + 10 min.)" +track: "Common Track" +title: "Verifying Stipula Legal Contracts in KeY" +slot: 19 +length: 30 +--- + +Stipula is an executable language that formalizes the operational semantics of legal contracts. It combines aspects from state automata, time, asynchronous and imperative programming. We sketch how a large class of Stipula programs can be modeled and formally verified in KeY. This is joint work with Cosimo Laneve (U Bologna) and Adele Veschetti. diff --git a/talks/heydari-tabar.md b/talks/heydari-tabar.md new file mode 100644 index 0000000..a00f929 --- /dev/null +++ b/talks/heydari-tabar.md @@ -0,0 +1,9 @@ +--- +author: "asmae.heydari-tabar@kit.edu" +kind: "Short Talk (10 min. + 5 min.)" +track: "Common Track, KeY-only Track" +title: "Data Dependence Logic: Applications" +slot: 15 +length: 30 +--- + diff --git a/talks/kamburjan.md b/talks/kamburjan.md new file mode 100644 index 0000000..3adaf3d --- /dev/null +++ b/talks/kamburjan.md @@ -0,0 +1,14 @@ +--- +author: "Eduard Kamburjan" +kind: "Regular Talk (20 min. + 10 min.)" +track: "KeY-only Track" +title: "Multi-perspective correctness of programs" +length: 30 +slot: 116 +--- + +Programs must be correct with respect to their application domain. Yet, current the program specification and verification approaches only consider correctness in terms of computations. +In this work, we present a Hoare Logic that manages two different perspectives on a program during a correctness proof: the computational view and the domain view. +This enables to not only specify the correctness of a program in terms of the domain without referring to the computational details, but also enables to interpret failed proof attempts in the domain. +For domain specification, we illustrate the use of description logics and base our approach on semantic lifting, a recently proposed approach to interpret a program as a knowledge graph. +We present a calculus that uses translations between both kinds of assertions, thus separating the concerns in specification, but enabling the use of description logic in verification. diff --git a/talks/katoen.md b/talks/katoen.md new file mode 100644 index 0000000..082e454 --- /dev/null +++ b/talks/katoen.md @@ -0,0 +1,10 @@ +--- +author: "Joost-Pieter Katoen" +kind: "Invited Talk (60 min.)" +length: 60 +track: "Common Track" +title: "Weakest Precondition Reasoning on Probabilistic Programs" +slot: 11 +--- + +Probabilistic programs encode randomised algorithms, robot controllers, learning components, security mechanisms, and much more. They are however hard to grasp. Not only by humans, also by computers: checking elementary properties related to e.g., termination are "more undecidable" than for ordinary programs. Although this all sounds like a no-go for automated analysis, I will present some non-trivial analyses of probabilistic programs using push-button technology. Our techniques are all based on weakest precondition reasoning. We will address automated techniques for run-time analysis, k-induction, and the synthesis of probabilistic loop invariants. diff --git a/talks/kern.md b/talks/kern.md new file mode 100644 index 0000000..94bf220 --- /dev/null +++ b/talks/kern.md @@ -0,0 +1,9 @@ +--- +author: "Philipp Kern" +kind: "Regular Talk (20 min. + 10 min.)" +track: "Common Track, KeY-only Track" +title: "TBD: Sth about NN Verification (probably verification of LSTMs)" +slot: 199 +length: 30 +--- + diff --git a/talks/klamroth.md b/talks/klamroth.md new file mode 100644 index 0000000..8aa1fee --- /dev/null +++ b/talks/klamroth.md @@ -0,0 +1,10 @@ +--- +author: "Jonas Klamroth" +kind: "Short Talk (10 min. + 5 min.)" +track: "Common Track" +title: "Leveraging Synergies in the Verification of Quantum and ML Software" +length: 15 +slot: 123 +--- + +Machine Learning and Quantum Computing must be recognized as the new technological frontiers, reshaping the landscape of computation across diverse fields. Their unreliable and highly complex nature, however, poses significant challenges regarding their use in practice as it requires rigorous verification to obtain formal guarantees of correctness. In classical software systems, verification was made possible by a series of principles (program decomposition, determinism, etc.) that no longer apply in quantum and ML software. In this paper, we examine similarities between the formal verification of quantum and ML software and identify common research directions. Particularly in the field of ML, there are ongoing research efforts, which we expect to generate synergies that can be exploited in the context of quantum software. We discuss significant overlaps and research opportunities and propose a close collaboration of those two fields in the future. diff --git a/talks/kodetzki.md b/talks/kodetzki.md new file mode 100644 index 0000000..e728803 --- /dev/null +++ b/talks/kodetzki.md @@ -0,0 +1,10 @@ +--- +author: "Maximilian Kodetzki" +kind: "Regular Talk (20 min. + 10 min.)" +track: "Common Track, KeY-only Track" +title: "Towards AI-assisted Correctness-by-Construction Software Development" +length: 30 +slot: 16 +--- + +In recent years, research in the field of artificial intelligence has made great progress. AI-tools are getting better in simulating human reasoning and behaviour every day. In this paper, we discuss the extent to which AI-tools can support Correctness-by-Construction engineering. This is an approach of formal methods to developing functionally correct programs incrementally on the basis of a formal specification. Using sound refinement rules, the correctness of the constructed program can already be guaranteed in the development process. We analyze the Correctness-by-Construction process regarding steps for potential AI-tool support in the tool CorC, which implements Correctness-by-Construction. We classify the findings in five areas of interest. Based on existing work, expert knowledge, and prototypical experiments, we discuss for each of the areas whether and to what extent AI-tools can support Correctness-by-Construction software development. We address the risk of AI-tools in formal methods and present our vision of AI-integration in the tool CorC to support developers in constructing programs using Correctness-by-Construction engineering. diff --git a/talks/lanziger.md b/talks/lanziger.md new file mode 100644 index 0000000..6e70610 --- /dev/null +++ b/talks/lanziger.md @@ -0,0 +1,12 @@ +--- +author: "Floran Lanzinger" +kind: "Regular Talk (20 min. + 10 min.)" +track: "Common Track, KeY-only Track" +title: "Types as Contracts: Scalable and Precise Verification" +length: 30 +slot: 114 +--- + +Refinement type systems allow programmers to use logical conditions to constrain admissible values of variables. However, most practical refinement type systems limit the expressiveness in the logic to remain automatically decidable and easy to use. Deductive verification tools, on the other hand, often come with expressive specification languages and powerful proof calculi that require interaction and scale badly with the program size. + +We introduce Kukicha, a refinement type system framework for Java that enables the interoperation of efficient type checking and deductive program verification. Kukicha combines refinement types with uniqueness types to track aliasing and packing types to track temporary violations. The use of a packing mechanism in combination with deductive verification allows Kukicha to be more expressive than similar type systems. Kukicha first performs an efficient syntactic well-typedness check. If this does not succeed, it emits a translated program where type annotations are replaced JML by specifications that can be proven in KeY. diff --git a/talks/laurent.md b/talks/laurent.md new file mode 100644 index 0000000..1dd1928 --- /dev/null +++ b/talks/laurent.md @@ -0,0 +1,14 @@ +--- +author: "Jonathan Laurent" +kind: "Regular Talk (20 min. + 10 min.)" +track: "Common Track" +title: "[Temporary Title] Few-Shot Programming: a new paradigm for programming with large language models" +length: 30 +slot: 18 +--- + +[Temporary abstract] Large-language models such as GPT4 have proved surprisingly good at solving a wide range of tasks from a handful of examples and at generating structured data such as programs or mathematical formulas. Yet, their lack of reliability puts a limit on their ability to solve large problems that require many steps of reasoning. + +Our work proposes a new programming paradigm called “few-shot programming”, where domain ex- perts write high-level problem-solving strategies in the form of nondeterministic programs whose choice-points are annotated with examples. This induces a search space that can be explored by querying large-language models for guidance. In addition, once enough examples are provided by humans for a strategy to bootstrap, this strategy can self-improve via an AlphaZero-like scheme, by solving a series of problems with search and extracting annotations from successful solutions. + +In this talk, we’ll introduce the “few-shot programming“ paradigm and demonstrate an early implementation prototype on an invariant-synthesis case study. diff --git a/talks/lohar.md b/talks/lohar.md new file mode 100644 index 0000000..cb9fc97 --- /dev/null +++ b/talks/lohar.md @@ -0,0 +1,12 @@ +--- +author: "Debasmita Lohar" +kind: "Regular Talk (20 min. + 10 min.)" +track: "Common Track" +title: "Towards Practical Analysis and Optimization for Finite-Precision" +length: 45/2 +slot: 22 +--- + +Finite-precision programs inevitably introduce numerical uncertainties due to input noises and finite-precision (roundoff) errors inherent in arithmetic operations. Furthermore, implementing these programs on hardware necessitates a trade-off between accuracy and efficiency. Therefore, it is crucial to ensure that numerical uncertainties remain acceptably small and to optimize implementations for accurate results tailored to specific applications. + +Existing analysis and optimization techniques for finite-precision often face challenges related to scalability and applicability in real-world scenarios. In this talk, I will provide a brief overview of my PhD research, which aimed to develop methods for handling input uncertainties and improving the scalability of the state-of-the-art, thus broadening their scope for practical applications. diff --git a/talks/longq.md b/talks/longq.md new file mode 100644 index 0000000..1b93c92 --- /dev/null +++ b/talks/longq.md @@ -0,0 +1,10 @@ +--- +author: "Long Qian" +kind: "Regular Talk (20 min. + 10 min.)" +track: "KeYmaera Track" +title: "Axiomatization of Compact Initial Value Problems: Open Properties" +slot: 215 +length: 30 +--- + +We prove the completeness of an axiomatization for initial value problems (IVPs) with compact initial conditions and compact time horizons for bounded open safety, open liveness and existence properties. This result is achieved via a computable procedure that generates symbolic proofs with differential invariants for rigorous error bounds of numerical solutions to such IVPs, bringing insights from symbolic logic and numerical analysis. As the axiomatization is a subset of the implemented axioms in Keymaera X, this also provides a theoretical justification for the verification power of Keymaera X. diff --git a/talks/nyholm.md b/talks/nyholm.md new file mode 100644 index 0000000..f4351de --- /dev/null +++ b/talks/nyholm.md @@ -0,0 +1,10 @@ +--- +author: "Joel Nyholm" +kind: "Short Talk (10 min. + 5 min.)" +track: "Common Track" +title: "A Bayesian energy profiler for Java system" +slot: 208 +length: 15 +--- + +Electricity is a vital infrastructural need for all. Reducing energy consumption would benefit economics, sustainability, and the environment in today's climate. However, to reduce consumption, one must know what one consumes. Therefore, we have developed a novel energy profiling system for Java applications. The profiler's basis is on measurements of iterative execution of small segments of Java code. We will then employ both a Bayesian and a summative estimation model to compare the accuracy of their estimates. Note that this is an ongoing paper. Hence, no results are yet available. diff --git a/talks/pascual.md b/talks/pascual.md new file mode 100644 index 0000000..2fc90d0 --- /dev/null +++ b/talks/pascual.md @@ -0,0 +1,8 @@ +--- +author: "romain.pascual@kit.edu" +kind: "Regular Talk (20 min. + 10 min.)" +track: "Common Track" +title: "Convide or Formal reasoning for geometric modeling" +length: 30 +--- + diff --git a/talks/pfeifer.md b/talks/pfeifer.md new file mode 100644 index 0000000..d94a8bd --- /dev/null +++ b/talks/pfeifer.md @@ -0,0 +1,9 @@ +--- +author: "Wolfram Pfeifer" +kind: "Regular Talk (20 min. + 10 min.)" +track: "Common Track, KeY-only Track" +title: "Observational Encapsulation: Abstracting Datastructures on the Heap into \"Singularities\"" +slot: 115 +length: 30 +--- + diff --git a/talks/platzer.md b/talks/platzer.md new file mode 100644 index 0000000..0dc9b4c --- /dev/null +++ b/talks/platzer.md @@ -0,0 +1,10 @@ +--- +author: "Andre Platzer" +kind: "Regular Talk (20 min. + 10 min.)" +track: "KeYmaera Track" +title: "Differential Hybrid Games" +slot: 213 +length: 30 +--- + +This talk introduces differential hybrid games, which combine differential games with hybrid games. In both kinds of games, two players interact with continuous dynamics. The difference is that hybrid games also provide all the features of hybrid systems and discrete games, but only deterministic differential equations. Differential games, instead, provide differential equations with input by both players, but not the luxury of hybrid games, such as mode switches and discrete or alternating interaction. This talk augments differential game logic with modalities for the combined dynamics of differential hybrid games. It shows how hybrid games subsume differential games and introduces differential game invariants and differential game variants for proving properties of differential games inductively. diff --git a/talks/scaletta.md b/talks/scaletta.md new file mode 100644 index 0000000..b26c0cd --- /dev/null +++ b/talks/scaletta.md @@ -0,0 +1,9 @@ +--- +author: "scaletta@cs.tu-darmstadt.de" +kind: "Short Talk (10 min. + 5 min.)" +track: "Common Track" +title: "Context-aware Contracts as a Lingua Franca for Behavioral Specification" +slot: 35 +length: 15 +--- + diff --git a/talks/schiffl.md b/talks/schiffl.md new file mode 100644 index 0000000..858e8c8 --- /dev/null +++ b/talks/schiffl.md @@ -0,0 +1,10 @@ +--- +author: "jonas.schiffl@kit.edu" +kind: "Short Talk (10 min. + 5 min.)" +track: "Common Track" +title: "What is Live? Temporal Properties in Smart Contract Applications" +slot: 33 +length: 15/30 +--- + +In my talk, I will discuss notions of safety and liveness in the adversarial domain of smart contract applications. I present a specification language for capturing relevant temporal properties in this domain. Furthermore, I discuss verification of these properties in the context of the SCAR smart contract application metamodel. diff --git a/talks/teuber.md b/talks/teuber.md new file mode 100644 index 0000000..89276ad --- /dev/null +++ b/talks/teuber.md @@ -0,0 +1,13 @@ +--- +author: "teuber@kit.edu" +kind: "Short or Regular Talk (please let me know which one)" +track: "Common Track" +title: "Heterogeneous Dynamic Logic" +length: 45/2 +slot: 21 +--- + +The novel framework of Heterogeneous Dynamic Logic presented in this talk allows the systematic combination of multiple program reasoning theories in dynamic logic, similar to the framework of satisfiability modulo theories (SMT) that allows the systematic combination of multiple theories in first-order logic. +Just like the foundation behind SMT are the conditions under which first-order theory combinations preserve decidability, the foundation here are the conditions under which program theory combinations preserve relative completeness. +The resulting combination principles are useful because they make it possible to modularly combine program reasoning on different levels and with different foci: +While preserving a clear separation of concerns between theories, we nonetheless enable a strong combination of insights across theories. diff --git a/talks/ulbrich.md b/talks/ulbrich.md new file mode 100644 index 0000000..21375fa --- /dev/null +++ b/talks/ulbrich.md @@ -0,0 +1,8 @@ +--- +author: "ulbrich@kit.edu" +kind: "Regular Talk (20 min. + 10 min.)" +track: "Common Track, KeY-only Track" +title: "" +length: 30 +--- + diff --git a/talks/ungzb.md b/talks/ungzb.md new file mode 100644 index 0000000..97590fa --- /dev/null +++ b/talks/ungzb.md @@ -0,0 +1,12 @@ +--- +author: "ungzb@student.kit.edu" +kind: "Short Talk (10 min. + 5 min.)" +track: "Common Track" +title: "Formal verification of verifiable, traceable and secret online elections" +slot: 193 +length: 15 +--- + +Online elections are especially vulnerable to external and internal threats compromising the privacy and integrity of the election. Thus, a voting system for online elections should enable the detection and correction of any errors in the election result — a property called strong software independence. +This can be achieved by risk-limiting audits, which however require adapting traditional privacy requirements for online elections so that sufficient evidence for the audits is produced. +In this talk, I present on-going work on the formalization and verification of secret and end-to-end-verifiable online elections that fulfill the traceability property necessary for post-election, risk-limiting audits, using the Tamarin prover. diff --git a/talks/uoxyc.md b/talks/uoxyc.md new file mode 100644 index 0000000..5e2f626 --- /dev/null +++ b/talks/uoxyc.md @@ -0,0 +1,9 @@ +--- +author: "uoxyc@student.kit.edu" +kind: "Short Talk (10 min. + 5 min.)" +track: "Common Track" +title: "Formal Verification of Symmetry Properties in Distance Rationalizable Voting Rules" +slot: 192 +length: 15 +--- + diff --git a/talks/veschetti.md b/talks/veschetti.md new file mode 100644 index 0000000..e1187ad --- /dev/null +++ b/talks/veschetti.md @@ -0,0 +1,10 @@ +--- +author: "adele.veschetti@tu-darmstadt.de" +kind: "Short Talk (10 min. + 5 min.)" +track: "Common Track" +title: "SmartML: Enhancing Security and Reliability in Smart Contract Development" +slot: 34 +length: 15/30 +--- + +Smart contracts, as integral components of blockchain technology, play a pivotal role in automating and executing agreements in a trust free manner. However, ensuring the correctness and reliability of smart contracts remains a significant challenge due to their complex nature and potential vulnerabilities. To address this challenge, we propose SmartML, a novel modeling language tailored specifically to smart contracts. This paper presents an in-depth exploration of the features, advantages, and applications of the proposed modeling language. By providing a precise and intuitive means of describing smart contract behaviors, SmartML aims to support the development, verification, and validation of smart contracts, ultimately bolstering trust and confidence in them. Furthermore, we discuss the relation to our modeling language with existing blockchain technologies and highlight its potential to streamline integration efforts. We posit SmartML as a versatile tool to advance, interoperability, reliability, and security of smart contracts in blockchain ecosystems.