From 002e181b5c00b05dcd3763a2cc2535a1e5ca2ce1 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sat, 20 Jul 2024 23:55:58 +0200 Subject: [PATCH] new program --- _layouts/programme.html | 216 ++++++++++++++++---------------------- _static/style.css | 78 ++++++++++++-- _static/style.scss | 138 ++++++++++++++++++++++++ config.yml | 2 +- render.py | 9 ++ requirements.txt | 1 + talks/abouelwafa.md | 1 + talks/ahrendt.md | 2 + talks/alvares.md | 1 + talks/beckert.md | 1 + talks/beyer.md | 1 + talks/blanchette.md | 1 + talks/bordis.md | 1 + talks/bubel.md | 1 + talks/buchholz.md | 1 + talks/cisasa.md | 1 + talks/closing.md | 1 + talks/degouw.md | 1 + talks/discussionllm.md | 1 + talks/drodt.md | 1 + talks/faerber.md | 10 ++ "talks/fr\303\244nzle.md" | 1 + talks/graetz.md | 1 + talks/granberry.md | 1 + talks/haehnle.md | 1 + talks/heydari-tabar.md | 3 +- talks/hiking_monday.md | 1 + talks/hiking_tuesday.md | 2 + talks/kabra.md | 1 + talks/kamburjan.md | 1 + talks/kern.md | 2 + talks/kodetzki.md | 1 + talks/lanzinger.md | 1 + talks/laurent.md | 1 + talks/lohar.md | 1 + talks/longq.md | 1 + talks/nyholm.md | 1 + talks/opening.md | 1 + talks/pascual.md | 5 +- talks/pfeifer.md | 1 + talks/platzer.md | 1 + talks/scaletta.md | 4 +- talks/schiffl.md | 1 + talks/teuber.md | 3 +- talks/ungzb.md | 1 + talks/uoxyc.md | 1 + talks/veschetti.md | 1 + 47 files changed, 365 insertions(+), 143 deletions(-) create mode 100644 _static/style.scss create mode 100644 talks/faerber.md diff --git a/_layouts/programme.html b/_layouts/programme.html index 7b397d6..f3f6fcc 100644 --- a/_layouts/programme.html +++ b/_layouts/programme.html @@ -15,8 +15,8 @@ {%endif%} {%- endmacro %} -{% macro session(name, chair, slots) -%} - +{% macro session(name, chair, slots, closed="") -%} + Session: {{name}} ∣ Chair: {{user(chair)}}
@@ -27,8 +27,9 @@ {% if slotId in bySlot %} {% set t = bySlot[slotId] %}

- + {{ t.meta.title }} {{ t.meta.length }} min.
@@ -42,6 +43,12 @@ {% endif %} {%- endmacro %} +{% macro entry(text,type) -%} +

+ {{ text }} +

+{%- endmacro %} + {% block content %}

Prelimniary Programme

@@ -52,89 +59,47 @@

more like a draft than final

that can be subscribed in your calender app

-
- - Day 0 - Monday, 29th July - + Day 0 - Monday, 29th July - - - - - + - + - - + + - - - + + + - + + - + +
#Time Topic
17:00 – 18:00Registration17:00 – 18:00 + {{ entry("Registration", "admin")}} +
18:00 –19:00Dinner at Haus der Kirche
18:00 – 19:00 + {{ entry("Dinner at Haus der Kirche", "break")}} +
19:00 –Getting Together19:00 – + {{entry("Getting Together at the bar", "social")}} +
20:00 – 21:00Meeting of the Programme Board20:00 – 21:00 + {{entry("Meeting of the Programme Board", "admin")}} +
@@ -142,87 +107,87 @@

more like a draft than final

Day 1 – Tuesday, 30th July - - - - - - - + + - + - + - - - + + + - + - - + + - + + - + + - + - + - - + + - + @@ -234,53 +199,53 @@

more like a draft than final

- Day 2 – Wednesday, 31th July + Day 2 – Wednesday, 31td July
#TopicTimeTopic
08:45 –09:0008:45 –09:00 {{ talk(10) }}
09:00 –10:3009:00 –10:30 - {{ session("Probabilism", "Alexander Weigl", [11,12,123]) }} + {{ session("Handling of Probabilistic Programs", "Alexander Weigl", [11,12,123], "closed") }}
10:30 – 11:00Coffee
10:30 – 11:00{{entry("Coffee", "break")}}
11:00 – 12:3011:00 – 12:30 - {{ session("Verification with Legal Aspects", "Wolfgang Ahrendt", [19,191,192,193,194]) }} + {{ session("Verification with Legal Aspects", "Richard Bubel", [19,191,192,193], "closed") }}
12:30 – 14:00Lunch12:30 – 14:00{{entry("Lunch", "break")}}
+ 14:00 – 15:30
Room: SR7+8 - - 		{{ session("#7a", "Mattias Ulbrich", [116,117,118]) }}{{ session("Case Studies in KeY", "Michael Kirsten", [116,117,118], "closed") }}
+ 14:00 – 15:30
Room: SR6 - - 		{{ session("#7b", "Andre Platzer", [216,217,218]) }}{{ session("#7b", "Yong Kiam Tan", [216,217,218]) }}
15:30 – 16:00 Coffee{{entry("Coffee", "break")}}
- 16:00 – 17:45 + 16:00 – 17:30
Room: SR7+8 		{{ session("#6a", "Richard Bubel", [113,114,115, 208]) }}{{ session("New Verification Methodologies with/in KeY", "Wojciech Mostowski", + [113,114,115], "closed") }}
16:00 – 17:45{{ session("#6b", "Enguerrand Prebet", [213,214,215,219]) }} + 16:00 – 17:45 +
+ Room: SR6 + 		{{ session("#6b", "Enguerrand Prebet", [219,214,213,215], "closed") }}
18:00 – 19:00Dinner at HdK {{entry("Dinner at Haus der Kirche", "break")}}
- - + + - - + + - - + + - - + + - + - - + + - - + + - - + + - + @@ -294,44 +259,45 @@

more like a draft than final

Day 3 – Thursday, 1st August
#TopicTimeTopic
09:00 –10:30{{ session("Formal Methods for CPS", "X", [20,21,22]) }}09:00 –10:30{{ session("Formal Methods for CPS", "Andre Platzer", [20,22,33]) }}
10:30 –11:00Coffee10:30 –11:00{{entry("Coffee", "break")}}
11:00 – 12:3011:00 – 12:30 - {{ session("#2", "X", [13,14,15]) }} + {{ session("“Efficient Analysis of Software Systems", "Bernhard Beckert", [13,14,15]) }}
12:30 – 14:00Lunch12:30 – 14:00{{entry("Lunch", "break")}}
14:00 – 15:30{{ session("#3", "X", [207,209]) }}14:00 – 15:30{{ session("Program Analyses of Software Systems", "Mattias Ulbrich", [207,209,208]) }}
15:30 – 16:00Coffee15:30 – 16:00{{entry("Coffee", "break")}}
16:00 – 18:0016:00 – 18:00 {{ session("Intersymbolic AI", "Ina Schaefer", [16,17,18,199,1999]) }}
- - - - - + + + + + + - - + + - + - - + +
#Time Topic
– 09:00Check-out!
09:00 – 10:45 - {{ session("Isabelle", "X", [30,31, 301, 34]) }} + {{ session("Isabelle", "Reiner Hähnle", [30,31, 301, 34]) }}
10:45 –11:10Coffee10:45 –11:15{{entry("Coffee", "break")}}
11:00 – 12:3011:00 – 12:15 - {{ session("#8", "X", [32,33,35,37]) }} + {{ session("#8", "Wolfang Ahrendt", [32,21,35]) }}
12:20 – 12:30 - {{ session("Closing", "—", [36]) }} + {{ talk(36) }}
12:30 – 14:00Lunch12:30 – {{ entry("Lunch", "break") }}
diff --git a/_static/style.css b/_static/style.css index 74eee0d..989ce98 100644 --- a/_static/style.css +++ b/_static/style.css @@ -1,6 +1,7 @@ main { padding:5em; - width:80em; + min-width:40em; + max-width:80em; margin:auto; } @@ -15,21 +16,76 @@ main { } -.track-key { - background: rgba(0,255,0,0.3); -} -.track-keymaera { - background: rgba(0,0,255,0.3); -} +ul { list-style:disc !important;} -.break { background: #666; color:white;} + .track-key { + background: rgba(0,255,0,0.2); + } + .track-keymaera { + background: rgba(0,0,255,0.2); + } -details {margin-bottom:2em;} -.slot:target { border: 1px solid red;} + details {margin-bottom:2em;} + .slot:target { border: 1px solid red;} -ul { list-style:disc !important;} + + .table tr td:first-child, + .table tr th:first-child + { + text-align: right; + border-bottom-width: 0pt; + } + + .slot { + padding:2ex; margin:0; + } + + .L15 {} + + p.L60, p.invited { /* invited talks */ + background: #5755d9; + color:white; + font-weight:bold; + } + + .L60 a { color:white; } + .L60 .chip a { color:black; } + + .social.slot { border-left: 3px solid green; } + .break.slot { border-left: 3px solid orange; + background: rgba(160,25,25,0.1); color:; + } + + summary { + font-size:100%; + } + + details.day > summary { + font-size:150%; + font-weight: bold; + margin: -0.5em -0.5em 0; + padding: 0.5em; + } + + details.day { + border: 1px solid #aaa; + border-radius: 4px; + padding: 0.5em 0.5em 0; + } + + .talks { + margin-left:10em; + margin-right:10em; + width:auto; + } + + .talk-entry { + border: 1px solid #5755d9; + margin-top:3ex; + padding: 2ex; + } diff --git a/_static/style.scss b/_static/style.scss new file mode 100644 index 0000000..6e8490b --- /dev/null +++ b/_static/style.scss @@ -0,0 +1,138 @@ +$color1: rgb(254, 243, 226); +$color2: rgb(190, 198, 160); +$color3: rgb(112, 136, 113); +$color4: rgb(96, 102, 118); + +$brown1: rgb(248, 244, 225); +$brown2: rgb(175, 143, 111); +$brown3: rgb(116, 81, 45); +$brown4: rgb(84, 51, 16); + +/* +rgb(108, 148, 111) +rgb(255, 211, 90) +rgb(255, 168, 35) +rgb(220, 0, 131) +*/ + +$social: darken(rgb(108, 148, 111),25); +$invitedTalk: rgb(220, 0, 131); +$break: rgb(108, 148, 111); +$ltalk:rgb(255, 211, 90); +$rtalk:rgb(255, 168, 35); + +main { + padding:5em; + min-width:40em; + max-width:80em; + margin:auto; +} + +.navbar { background: $color3; padding:1ex;} +.navbar a, .navbar .btn.btn-link { color: white; } +.hero { + background: rgb(25,55,25); + color:white; + background-repeat: no-repeat; + background-attachment: fixed; + background-position: right bottom; +} + +ul { + list-style:disc !important; +} + +.track-key { + background: $color2; +} + +.track-keymaera { + background: rgb(180,180,200); +} + + +details { + margin-bottom:2em; +} + +.table tr td:first-child, +.table tr th:first-child +{ + text-align: right; + border-bottom-width: 0pt; + font-weight:bold; + width:30%; +} + +$bsz: 3ex; + +span.session { + font-weight:bold; +} + +span.session.closed:before { + content:"🔒"; +} + +.slot { + padding:2ex; margin:0; + + border-left: $bsz solid white; + + + :target { + border-top: 2px solid red; + border-bottom: 2px solid red; + } + + &.L60, &.invited { /* invited talks */ + border-left: $bsz solid $invitedTalk; + font-weight:bold; + } + &.social { border-left: $bsz solid $social; } + &.break { + border-left: $bsz solid $break; + background: --darker(160,25,25,0.1); + } + + &.L30, &.L25 { border-left: $bsz solid $rtalk; } + &.L15 { border-left: $bsz solid $ltalk; } + + &.admin { + border-left: $bsz solid #444; + } +} + + +summary { + font-size:100%; +} + +details.day > summary { + font-size:150%; + font-weight: bold; + margin: -0.5em -0.5em 0; + padding: 0.5em; +} + +details.day { + border: 1px solid #aaa; + border-radius: 4px; + padding: 0.5em 0.5em 0; +} + +.talks { + margin-left:10em; + margin-right:10em; + width:auto; +} + +.talk-entry { + border: 1px solid #5755d9; + margin-top:3ex; + padding: 2ex; +} + +.talks img { + width:100%; +} diff --git a/config.yml b/config.yml index 100da23..30c3faf 100644 --- a/config.yml +++ b/config.yml @@ -61,7 +61,7 @@ persons: link: "" "Aditi Kabra": mail: "akabra@andrew.cmu.edu" - link: "" + link: "https://aditink.github.io/" "Eduard Kamburjan": mail: "eduard@ifi.uio.no" link: "" diff --git a/render.py b/render.py index 31697cd..6a7ec45 100755 --- a/render.py +++ b/render.py @@ -88,6 +88,14 @@ def render_program(): fh.write(template.render(content=p.content, page=p.meta, talks=talks, bySlot=bySlot, site=SITE)) +def render_css(): + import sass + content = sass.compile(dirname=("_static","public"), output_style="compressed") + print(content) + #with open(PUBLIC/"style.css", 'w') as fh: + # fh.write(content) + + def main(): if PUBLIC.exists(): @@ -96,6 +104,7 @@ def main(): os.system("cp -R _static/* public") + render_css() render_index() render_registration() render_locations() diff --git a/requirements.txt b/requirements.txt index d2d1ad2..20f7aea 100644 --- a/requirements.txt +++ b/requirements.txt @@ -1,3 +1,4 @@ jinja2 markdown2 icalendar +libsass diff --git a/talks/abouelwafa.md b/talks/abouelwafa.md index 88936de..3a1e92c 100644 --- a/talks/abouelwafa.md +++ b/talks/abouelwafa.md @@ -5,5 +5,6 @@ track: "KeYmaera Track" title: "tbd" slot: 216 length: 30 +order: 34 --- diff --git a/talks/ahrendt.md b/talks/ahrendt.md index c3e6c10..abf6a31 100644 --- a/talks/ahrendt.md +++ b/talks/ahrendt.md @@ -5,5 +5,7 @@ track: "KeYmaera Track" title: "On proving that an unsafe controller is not proven safe" slot: 219 length: 15 +order: 36 --- + Formal verification of cyber-physical systems is one way to guarantee safety. However, care must be taken because modelling errors might result in proving a faulty controller safe, which is potentially catastrophic in practice. We deal with two such modelling errors in differential dynamic logic, and provide conditions under which these two modelling errors cannot cause a faulty controller to be proven safe. We also show how these conditions can be proven with help of KeYmaera X. diff --git a/talks/alvares.md b/talks/alvares.md index c836dab..3af7683 100644 --- a/talks/alvares.md +++ b/talks/alvares.md @@ -5,6 +5,7 @@ track: "KeY-only Track" title: "Modeling Solidity data types in SolidiKeY" slot: 193 length: 30 +order: 23 --- Solidity, the main programming language for smart contracts in cryptocurrencies, is being formalized in KeY. diff --git a/talks/beckert.md b/talks/beckert.md index 9e3a1cb..af88b44 100644 --- a/talks/beckert.md +++ b/talks/beckert.md @@ -5,5 +5,6 @@ track: "Common Track, KeY-only Track" title: "tbd." slot: 199 length: 15 +order: 76 --- diff --git a/talks/beyer.md b/talks/beyer.md index 96d432a..84797d7 100644 --- a/talks/beyer.md +++ b/talks/beyer.md @@ -6,4 +6,5 @@ title: "tbd" slot: 207 length: 60 type: invited +order: 70 --- diff --git a/talks/blanchette.md b/talks/blanchette.md index d66ff67..a36f6bc 100644 --- a/talks/blanchette.md +++ b/talks/blanchette.md @@ -6,6 +6,7 @@ title: "Formalizing Saturation, Resolution, and Superposition in Isabelle/HOL" slot: 30 length: 60 type: invited +order: 100 --- Resolution and superposition are prime examples of proof systems implemented in saturation-based theorem provers. These have a rich metatheory, which both is interesting in its own right and partly explains why the provers perform well in practice. My collegues and I formalized the soundness and completeness proofs of resolution and superposition in Isabelle/HOL. In addition, we developed a so-called saturation framework, on paper and in Isabelle, that makes such proofs easier to carry out and more modular. diff --git a/talks/bordis.md b/talks/bordis.md index 936827e..67f4be1 100644 --- a/talks/bordis.md +++ b/talks/bordis.md @@ -5,6 +5,7 @@ track: "Common Track" title: "Free Facts: An Alternative to Inefficient Axioms in Dafny" slot: 15 length: 30 +order: 63 --- 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. diff --git a/talks/bubel.md b/talks/bubel.md index feeae74..f3d6c6e 100644 --- a/talks/bubel.md +++ b/talks/bubel.md @@ -5,6 +5,7 @@ track: "KeY-only Track" title: "Verification of the Norway Election Algorithm" slot: 118 length: 30 +order: 33 --- 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 index d869fe6..7938793 100644 --- a/talks/buchholz.md +++ b/talks/buchholz.md @@ -5,6 +5,7 @@ track: "KeY-only Track" title: "Transferring proof obligations from KeY to Isabelle/HOL" slot: 31 length: 15 +order: 101 --- *Can be reduced to short talk if necessary* diff --git a/talks/cisasa.md b/talks/cisasa.md index cef9542..812007b 100644 --- a/talks/cisasa.md +++ b/talks/cisasa.md @@ -5,6 +5,7 @@ track: "KeYmaera Track" title: "Formal Verification of 2-Element Lumped-Capacitance Model" slot: 217 length: 30 +order: 33 --- We show a verified controller that regulates a heat exchange system. diff --git a/talks/closing.md b/talks/closing.md index 218d8f9..214752a 100644 --- a/talks/closing.md +++ b/talks/closing.md @@ -7,6 +7,7 @@ title: "Closing Cerenomy" slot: 36 length: 10 order: 999 +type: admin --- Closing cerenomy diff --git a/talks/degouw.md b/talks/degouw.md index 0d2ea44..27913e7 100644 --- a/talks/degouw.md +++ b/talks/degouw.md @@ -5,6 +5,7 @@ track: "Common Track, KeY-only Track" title: "Analyzing OpenJDK's BitSet" slot: 117 length: 30 +order: 31 --- 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/discussionllm.md b/talks/discussionllm.md index bfef75f..3e2a7ed 100644 --- a/talks/discussionllm.md +++ b/talks/discussionllm.md @@ -5,5 +5,6 @@ track: "Common Track, KeY-only Track" title: "Discussion" slot: 1999 length: 30 +order: 77 --- diff --git a/talks/drodt.md b/talks/drodt.md index 7f58f1f..fe85218 100644 --- a/talks/drodt.md +++ b/talks/drodt.md @@ -5,6 +5,7 @@ track: "Common Track, KeY-only Track" title: "Rusty KeY" length: 30 slot: 113 +order: 34 --- TBD diff --git a/talks/faerber.md b/talks/faerber.md new file mode 100644 index 0000000..30dae86 --- /dev/null +++ b/talks/faerber.md @@ -0,0 +1,10 @@ +--- +author: "Henriette Färber" +kind: "Short Talk (10 min. + 5 min.)" +track: "Common Track" +title: "Towards Recovery from Inconsistency in V-SUMs" +slot: 33 +length: 15 +order: 62 +--- + diff --git "a/talks/fr\303\244nzle.md" "b/talks/fr\303\244nzle.md" index 8cdee3b..dc08c91 100644 --- "a/talks/fr\303\244nzle.md" +++ "b/talks/fr\303\244nzle.md" @@ -4,6 +4,7 @@ title: "Why does so much CPS design go on without much formal methods? A plea fo slot: 20 type: invited length: 45 +order: 60 --- 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 index 520ed67..3fcf716 100644 --- a/talks/graetz.md +++ b/talks/graetz.md @@ -5,5 +5,6 @@ track: "Common Track" title: "Single Path Verification for Validation or Debugging" slot: 14 length: 30 +order: 62 --- diff --git a/talks/granberry.md b/talks/granberry.md index a48e9e3..7674a14 100644 --- a/talks/granberry.md +++ b/talks/granberry.md @@ -5,6 +5,7 @@ track: "KeY-only Track" title: "Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods" length: 25 slot: 17 +order: 74 --- 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 index c7dca89..a20979c 100644 --- a/talks/haehnle.md +++ b/talks/haehnle.md @@ -5,6 +5,7 @@ track: "Common Track" title: "Verifying Stipula Legal Contracts in KeY" slot: 19 length: 30 +order: 20 --- 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 index 43966d0..32e21ae 100644 --- a/talks/heydari-tabar.md +++ b/talks/heydari-tabar.md @@ -4,6 +4,7 @@ kind: "Short Talk (10 min. + 5 min.)" track: "Common Track, KeY-only Track" title: "Data Dependence Logic: Applications" slot: 209 -length: 30 +length: 15 +order: 71 --- diff --git a/talks/hiking_monday.md b/talks/hiking_monday.md index 4a1e184..0d05459 100644 --- a/talks/hiking_monday.md +++ b/talks/hiking_monday.md @@ -4,6 +4,7 @@ title: "Black Forest Hike with Panoramic Views" slot: 999 type: social order: -1 +length: 300 --- For those who want to get some panoramic views of the area and, if weather permits, through the Rhine valley up to the Vosges, we organize a voluntary hike on Monday afternoon just before the symposium officially starts. The hike is of medium difficulty and leads us about 9 km distance and 260 m elevation through the Northern Black Forest on a former border trail between Baden and Württemberg marked by ancient rock formations that go back to the Triassic. In order to get to and from the start and end point of the hike, we will optionally take a short bus ride. There is also the option of a detour of roughly 2 km to pass by the gorgeous Falkensteinfelsen with views on Bad Herrenalb. diff --git a/talks/hiking_tuesday.md b/talks/hiking_tuesday.md index 3eeb57f..15aedc0 100644 --- a/talks/hiking_tuesday.md +++ b/talks/hiking_tuesday.md @@ -3,6 +3,8 @@ author: "Organization by Jonas Schiffl" title: "Paseo to Frauenalb" slot: 998 type: social +length: 120 +order: 50 --- On Tuesday evening and good weather, there will be a light walk (paseo, Spaziergang) to the ruined abbey of Frauenalb. Frauenalb is a smaller village two train station before Bad Herrenalb. You have the possibility to *cheat* by using the tram (most probably we will go down the hill and come back with the tram). Of course, this is not mandatory, and of course the weather should be suitable for the walk. The distance is roughly 6km w/o steep up and downs. diff --git a/talks/kabra.md b/talks/kabra.md index 504f294..9e3cc2a 100644 --- a/talks/kabra.md +++ b/talks/kabra.md @@ -5,5 +5,6 @@ track: "KeYmaera Track" title: "Control Envelope Synthesis in KeYmaera X" slot: 214 length: 30 +order: 38 --- diff --git a/talks/kamburjan.md b/talks/kamburjan.md index 3adaf3d..a65e6b2 100644 --- a/talks/kamburjan.md +++ b/talks/kamburjan.md @@ -5,6 +5,7 @@ track: "KeY-only Track" title: "Multi-perspective correctness of programs" length: 30 slot: 116 +order: 30 --- 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. diff --git a/talks/kern.md b/talks/kern.md index 69d0878..2e90310 100644 --- a/talks/kern.md +++ b/talks/kern.md @@ -4,5 +4,7 @@ kind: "Regular Talk (20 min. + 10 min.)" track: "Common Track, KeY-only Track" title: "TBD: Sth about NN Verification (probably verification of LSTMs)" length: 30 +slot: 32 +order: 104 --- diff --git a/talks/kodetzki.md b/talks/kodetzki.md index 69caa33..d960b1a 100644 --- a/talks/kodetzki.md +++ b/talks/kodetzki.md @@ -5,6 +5,7 @@ track: "Common Track, KeY-only Track" title: "Towards AI-assisted Correctness-by-Construction Software Development" length: 25 slot: 16 +order: 73 --- 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/lanzinger.md b/talks/lanzinger.md index 090d371..2a5aac5 100644 --- a/talks/lanzinger.md +++ b/talks/lanzinger.md @@ -5,6 +5,7 @@ track: "Common Track, KeY-only Track" title: "Types as Contracts: Scalable and Precise Verification" length: 30 slot: 114 +order: 35 --- 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. diff --git a/talks/laurent.md b/talks/laurent.md index b8b754e..8fa84b9 100644 --- a/talks/laurent.md +++ b/talks/laurent.md @@ -5,6 +5,7 @@ track: "Common Track" title: "[Temporary Title] Few-Shot Programming: a new paradigm for programming with large language models" length: 25 slot: 18 +order: 74 --- [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. diff --git a/talks/lohar.md b/talks/lohar.md index adccb1a..ae71240 100644 --- a/talks/lohar.md +++ b/talks/lohar.md @@ -5,6 +5,7 @@ track: "Common Track" title: "Towards Practical Analysis and Optimization for Finite-Precision" length: 30 slot: 13 +order: 70 --- 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. diff --git a/talks/longq.md b/talks/longq.md index 1b93c92..28d958e 100644 --- a/talks/longq.md +++ b/talks/longq.md @@ -5,6 +5,7 @@ track: "KeYmaera Track" title: "Axiomatization of Compact Initial Value Problems: Open Properties" slot: 215 length: 30 +order: 40 --- 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 index f4351de..f583876 100644 --- a/talks/nyholm.md +++ b/talks/nyholm.md @@ -5,6 +5,7 @@ track: "Common Track" title: "A Bayesian energy profiler for Java system" slot: 208 length: 15 +order: 72 --- 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/opening.md b/talks/opening.md index d4b095a..154fdd3 100644 --- a/talks/opening.md +++ b/talks/opening.md @@ -4,6 +4,7 @@ title: "Opening Cerenomy" slot: 10 length: 15 order: 10 +type: admin --- Open cerenomy diff --git a/talks/pascual.md b/talks/pascual.md index face570..c936199 100644 --- a/talks/pascual.md +++ b/talks/pascual.md @@ -2,8 +2,9 @@ author: "Romain Pascual" kind: "Regular Talk (20 min. + 10 min.)" track: "Common Track" -title: "Convide or Formal reasoning for geometric modeling" -length: 22 +title: "Convide tbd." +length: 30 slot: 22 +order: 61 --- diff --git a/talks/pfeifer.md b/talks/pfeifer.md index d94a8bd..5a0bfad 100644 --- a/talks/pfeifer.md +++ b/talks/pfeifer.md @@ -5,5 +5,6 @@ track: "Common Track, KeY-only Track" title: "Observational Encapsulation: Abstracting Datastructures on the Heap into \"Singularities\"" slot: 115 length: 30 +order: 35 --- diff --git a/talks/platzer.md b/talks/platzer.md index 205b55f..32abfae 100644 --- a/talks/platzer.md +++ b/talks/platzer.md @@ -5,6 +5,7 @@ track: "KeYmaera Track" title: "Differential Hybrid Games" slot: 213 length: 30 +order: 39 --- 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 index 08ff419..5d9ed54 100644 --- a/talks/scaletta.md +++ b/talks/scaletta.md @@ -1,9 +1,9 @@ --- -author: "scaletta@cs.tu-darmstadt.de" +author: "Marco Scaletta" kind: "Short Talk (10 min. + 5 min.)" track: "Common Track" title: "Context-aware Contracts as a Lingua Franca for Behavioral Specification" -slot: 194 +slot: 35 length: 15 --- diff --git a/talks/schiffl.md b/talks/schiffl.md index 6801b17..135e7fb 100644 --- a/talks/schiffl.md +++ b/talks/schiffl.md @@ -5,6 +5,7 @@ track: "Common Track" title: "What is Live? Temporal Properties in Smart Contract Applications" slot: 192 length: 15 +order: 22 --- 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 index 8a47d69..037f782 100644 --- a/talks/teuber.md +++ b/talks/teuber.md @@ -3,8 +3,9 @@ author: "Samuel Teuber" kind: "Short or Regular Talk (please let me know which one)" track: "Common Track" title: "Heterogeneous Dynamic Logic" -length: 22 +length: 30 slot: 21 +order: 105 --- 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. diff --git a/talks/ungzb.md b/talks/ungzb.md index edfab01..73a2f98 100644 --- a/talks/ungzb.md +++ b/talks/ungzb.md @@ -5,6 +5,7 @@ track: "Common Track" title: "Formal verification of verifiable, traceable and secret online elections" slot: 301 length: 15 +order: 102 --- 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. diff --git a/talks/uoxyc.md b/talks/uoxyc.md index 1ddd26a..9fd10f4 100644 --- a/talks/uoxyc.md +++ b/talks/uoxyc.md @@ -5,5 +5,6 @@ track: "Common Track" title: "Formal Verification of Symmetry Properties in Distance Rationalizable Voting Rules" slot: 34 length: 15 +order: 103 --- diff --git a/talks/veschetti.md b/talks/veschetti.md index fa677ef..5a5eb1d 100644 --- a/talks/veschetti.md +++ b/talks/veschetti.md @@ -5,6 +5,7 @@ track: "Common Track" title: "SmartML: Enhancing Security and Reliability in Smart Contract Development" slot: 191 length: 15 +order: 21 --- 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.