Blogs (1) >>
ICSE 2019
Sat 25 - Fri 31 May 2019 Montreal, QC, Canada
Mon 27 May 2019 14:40 - 15:05 at Foyer - Session 3 Chair(s): Eunsuk Kang

In this paper, we use the process algebra CSP and the formal model-checker FDR to show that the implementation of one-to-one channel communication in the process-oriented language ProcessJ is correct. ProcessJ is a new process-oriented language with Java-like syntax and CSP-based communication using synchronous channels. ProcessJ allows for hundreds of millions of processes to be executed on a single processor core. ProcessJ generates Java code which eventually runs concurrently on the JVM using a cooperative scheduler. We use the translation from the ProcessJ code generator to translate ProcessJ to Java and further into CSP. We then utilize the FDR model-checker to show that the generated Java code behaves like a generic synchronous, blocking, non-buffered one-to-one channel used previously to show the correctness of channel communication in JCSP – a Java library that supports JVM thread-based concurrency. Finally, we highlight a lesson from verifying our behaviour using FDR – the ability to simplify our approach and show the implementation still meets our specification.

Mon 27 May

Displayed time zone: Eastern Time (US & Canada) change

14:00 - 15:30
Session 3FormaliSE at Foyer
Chair(s): Eunsuk Kang Carnegie Mellon University
Parallelizable Reachability Analysis Algorithms for Feed-Forward Neural Networks
Hoang-Dung Tran Vanderbilt University, Patrick Musau Vanderbilt University, Diego Manzanas Lopez Vanderbilt University, Xiao Dong Yang Vanderbilt University, Luan Nguyen University of Pennsylvania, Weiming Xiang Vanderbilt University, Taylor T Johnson Vanderbilt University
Towards Sampling and Simulation-Based Analysis of Featured Weighted Automata
Maxime Cordy SnT, University of Luxembourg, Axel Legay , Sami Lazreg Visteon Electronics and Universite Cote d Azur, Philippe Collet University of Nice
Verifying Channel Communication Correctness for a Multi-Core Cooperatively Scheduled Runtime Using CSP
Jan Pedersen University of Nevada Las Vegas, Kevin Chalmers Edinburgh Napier University
A Generalized Program Verification Workflow Based on Loop Elimination and SA Form
Cláudio Belo Lourenço LRI, Université Paris-Sud & INRIA Saclay, Maria João Frade HASLab/INESC TEC & Universidade do Minho, Portugal, Jorge Sousa Pinto HASLab/INESC TEC & Universidade do Minho, Portugal