Empower - The Campaign for Northeastern University


Resource-Parameterized Program Analysis using Observation Sequences

Title: Resource-Parameterized Program Analysis using Observation SequencesSpeaker: Peizun Liu, PhD Student at Northeastern UniversityDate: October 30, 2018Time: 12:00PM - 2:00PMLocation: ISEC 138, 805 Columbus Avenue, Boston, MA 02120 AbstractMost programs are naturally designed over a variable number of discrete resources, which can be either physical components like threads or logical entities like context switches. Such a resource is typically parametric, where the value of the parameter varies across different execution environments and is unknown at design time. We call such programs resource-parameterized. Although highly desirable, formally analyzing resource-parameterized programs for various error conditions is notoriously hard or even undecidable. Some existing research imposes bounds on certain resources, such as the number of available execution threads or thread contexts, to tackle the intractability or sidestep the undecidability of the analysis. This leads to a series of incomplete techniques that are believed to catch "most bugs" in practice. The question of whether these techniques can also prove the absence of bugs, however, has remained open in many cases.We address this question by introducing a broad verification methodology, the paradigm of observation sequences, for resource-parameterized programs. The verification is conducted by observing how changes to the resource parameter affect the behavior of the considered program. Applied to the undecidable problem of context-parameterized analysis for procedural concurrent programs, the paradigm results in partial verification techniques: they may not terminate, but are able to both refute and prove safety for concurrent recursive threads. Experiments have shown the effectiveness of our techniques. The paradigm of observation sequences is designed with generality in mind. In this proposal, we plan to explore two more instances: one is the queue-parameterized analysis for message-passing programs which communicate via queued messages; the other is access-parameterized analysis for shared-memory multithreaded programs. Both generalizations are supported by tool development and empirical evaluation. About the SpeakerPeizun Liu is a PhD student in Computer Science at Northeastern University's College of Computer and Information Science, advised by Prof. Thomas Wahl. His research interests lie in the areas of formal verification and program analysis. Peizun received his Master's degree in Software Engineering from Tsinghua University and his Bachelor's degree in Information Management & Information System from Chengdu University of Technology. Thesis Committee Prof. Thomas Wahl (Thesis Advisor) Prof. Cristina Nita-Rotaru Prof. Jan Vitek Dr. Akash Lal (External Member)

Tuesday, October 30, 2018 at 12:00pm



Google Calendar iCal Outlook

Recent Activity