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
Times are displayed in time zone: Eastern Time (US & Canada) change

14:00 - 15:30: Session 3FormaliSE at Foyer
Chair(s): Eunsuk KangCarnegie Mellon University
14:00 - 14:25
Parallelizable Reachability Analysis Algorithms for Feed-Forward Neural Networks
Hoang-Dung TranVanderbilt University, Patrick MusauVanderbilt University, Diego Manzanas LopezVanderbilt University, Xiao Dong YangVanderbilt University, Luan NguyenUniversity of Pennsylvania, Weiming XiangVanderbilt University, Taylor T JohnsonVanderbilt University
14:25 - 14:40
Towards Sampling and Simulation-Based Analysis of Featured Weighted Automata
Maxime CordySnT, University of Luxembourg, Axel Legay, Sami LazregVisteon Electronics and Universite Cote d Azur, Philippe ColletUniversity of Nice
14:40 - 15:05
Verifying Channel Communication Correctness for a Multi-Core Cooperatively Scheduled Runtime Using CSP
Jan PedersenUniversity of Nevada Las Vegas, Kevin ChalmersEdinburgh Napier University
15:05 - 15:30
A Generalized Program Verification Workflow Based on Loop Elimination and SA Form
Cláudio Belo LourençoLRI, Université Paris-Sud & INRIA Saclay, Maria João FradeHASLab/INESC TEC & Universidade do Minho, Portugal, Jorge Sousa PintoHASLab/INESC TEC & Universidade do Minho, Portugal