May 2020 - Annonce

[Last CfP] Onward! Essays @SPLASH 2020, Chicago, Nov 15-20
by Didier Verna 19 May '20

19 May '20

Onward! Essays 2020 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software Renaissance Chicago Downtown Hotel Chicago, USA November 15--20 2020 Part of SPLASH 2020 Systems, Programming Languages and Applications: Software for Humanity https://2020.splashcon.org/track/splash-2020-Onward-essays 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 examples. 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. Important dates: 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 Programme Committee: 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

1 0

New publication: LTL Model Checking for Communicating Concurrent Programs
by adrien 15 May '20

15 May '20

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 Abstract: 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.

1 0

New publication: Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-Determinization
by Alexandre Duret-Lutz 14 May '20

14 May '20

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 https://www.lrde.epita.fr/wiki/Publications/blahoudek.20.atva Abstract: 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. -- Alexandre Duret-Lutz

1 0