BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//University of Liverpool Computer Science Seminar System//v2//EN
BEGIN:VEVENT
DTSTAMP:20260921T003248Z
UID:Seminar-verification-665@lxserverM.csc.liv.ac.uk
ORGANIZER:CN=Patrick Totzke:MAILTO:totzke@liverpool.ac.uk
DTSTART:20180510T140000
DTEND:20180510T150000
SUMMARY:Verification Series
DESCRIPTION:Matthew Luckcuck: Using Circus to Verify Safety-Critical Java Level 2 Programs\n\nSafety-Critical Java (SCJ) is a Java-based programming language designed for real-time and safety-critical programs. It has been developed from the Real-Time Specification for Java. SCJ provides a strict memory- and programming- model. SCJ is organised into three ascending levels of complexity from Level 0 (the simplest) to Level 2 (the most complex).\n\nThis work makes three contributions to the state of the art on veri?cation of SCJ Level 2 programs. Firstly, I model the SCJ Level 2 paradigm using the state-rich process algebra Circus. My model can be used to identify potential errors in the programs that it represents. Secondly, because I model the API separately from the program-speci?c behaviour, my model can be used to show that the SCJ API does not introduce undesirable behaviour, such as deadlock or livelock. Finally, my model enables several options for verifying SCJ Level 2 programs.\n\n\nhttps://www.csc.liv.ac.uk/research/seminars/abstract.php?id=665
LOCATION:
END:VEVENT
END:VCALENDAR