Onward! Essays 2020
ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and
Reflections on Programming and Software
Renaissance Chicago Downtown Hotel
November 15--20 2020
Part of SPLASH 2020
Systems, Programming Languages and Applications:
Software for Humanity
Onward! is a premier multidisciplinary conference focused on everything to
do with programming and software: including processes, methods, languages,
communities, applications and education.
Compared to other conferences, Onward! is more radical, more visionary, and
more open to ideas that are well-argued but not yet proven. It is not
looking for research-as-usual papers. To allow room for bigger, bolder
and/or less mature ideas, it accepts less exact methods of validation, such
as compelling arguments, exploratory implementations, and substantial
Onward! Essays is looking for clear and compelling pieces of writing about
topics important to the software community (there is also a parallel Papers
track with a seperate announcement).
An essay can be an exploration of the topic and its impact, or a story about
the circumstances of its creation; it can present a personal view of what
is, explore a terrain, or lead the reader in an act of discovery; it can be
a philosophical digression or a deep analysis. It can describe a personal
journey, perhaps the one the author took to reach an understanding of the
topic. The subject area—software, programming, and programming
languages—should be interpreted broadly and can include the relationship of
software to human endeavors, or its philosophical, sociological,
psychological, historical, or anthropological underpinnings.
Format and Selection:
Onward! essays must describe unpublished work that is not currently
submitted for publication elsewhere as described by SIGPLAN's Republication
Policy. Submitters should also be aware of ACM's Policy and Procedures on
Plagiarism. Onward! essays should use the ACM SIGPLAN Conference acmart
format. Please refer to the conference's website above for full details.
The Onward! Essays track follows a two-phase review process. Essays are
peer-reviewed in a single-blind manner. Accepted essays will appear in the
Onward! Proceedings in the ACM Digital Library, and must be presented at the
conference. Submissions will be judged on the potential impact of the ideas
and the quality of the presentation.
All deadlines are midnight, anywhere on Earth.
Essay submission: 23 May
First-round notification: 11 July
Second-round submission: 15 August
Final notification: 30 August
Conference: 15--20 November
Didier Verna, EPITA Research lab, France (Program Chair)
Anya Helene Bagge, University of Bergen, Norway
Alexandre Bergel, University of Chile
Jean Bresson, Ableton, Germany
Maxime Chevalier-Boisvert, Université de Montréal, Québec
Elisa Gonzalez Boix, Vrije Universiteit Brussel, Belgium
Hidehiko Masuhara, Tokyo Institute of Technology, Japan
Kent Pitman, PTC, USA
Donya Quick, Stevens Institute of Technology, USA
Gordana Rakić, University of Novi Sad, Serbia
Resistance is futile. You will be jazzimilated.
Lisp, Jazz, Aïkido: http://www.didierverna.info
I am happy to announce that the following paper has been accepted in the
Innovations in Systems and Software Engineering (ISSE) journal.
LTL Model Checking for Communicating Concurrent Programs
Adrien Pommellet and Tayssir Touili
We present in this paper a new approach to the static analysis of
concurrent programs with procedures. To this end, we model
multi-threaded programs featuring recursive procedure calls and
synchronisation by rendez-vous between parallel threads with
communicating pushdown systems (from now on CPDSs).
The reachability problem for this particular class of automata is
unfortunately undecidable. However, it has been shown that an efficient
abstraction of the execution traces language can nonetheless be
computed. To this end, an algebraic framework to over-approximate
context-free languages has been introduced by Bouajjani et al.
In this paper, we combine this framework with an automata-theoretic
approach in order to approximate an answer to the model checking problem
of the linear-time temporal logic (from now on LTL) on CPDSs. We then
present an algorithm that, given a single-indexed or stutter-invariant
LTL formula, allows us to prove that no run of a CPDS verifies this
formula if the procedure ends.
I am happy to announce that the following paper has been accepted at
the 32nd International Conference on Computer-Aided Verification (CAV'20),
to be held virtually in July 2020.
Seminator 2 Can Complement Generalized Büchi Automata
via Improved Semi-Determinization
František Blahoudek¹, Alexandre Duret-Lutz², Jan Strejček³
¹University of Texas at Austin, USA
²LRDE, EPITA, Le Kremlin-Bicêtre, France
³Faculty of Informatics, Masaryk University, Brno, Czech Republic
We present the second generation of the tool Seminator that
transforms transition-based generalized Büchi automata (TGBAs)
into equivalent semi-deterministic automata. The tool has been
extended with numerous optimizations and produces considerably
smaller automata than its first version. In connection with the
state-of-the-art LTL to TGBAs translator Spot, Seminator 2
produces smaller (on average) semi-deterministic automata than the
direct LTL to semi-deterministic automata translator ltl2ldgba of
the Owl library. Further, Seminator 2 has been extended with an
improved NCSB complementation procedure for semi-deterministic
automata, providing a new way to complement automata that is
competitive with state-of-the-art complementation tools.