PRECISE members win Test-of-Time Award
November 4, 2019

PRECISE members Insup Lee and Oleg Sokolsky, along with Sampath Kannan, Moonzoo Kim, and Mahesh Viswanathan, win the Test-of-Time Award for their 2001 paper "Java-MaC: a run-time assurance tool for Java programs" at the 2019 Conference on Runtime Verification.



PRECISE's team won best paper award at Memocode
October 10, 2019

Luan Nguyen, Gautam Mohan, James Weimer, Oleg Sokolsky, Insup Lee and Rajeev Alur won Best Paper Award on their "Detecting Security Leaks in Hybrid Systems with Information Flow Analysisat ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE), 2019.  

Congratulations to Luan and all!


Our "Control of Multi-Drone Fleets with Temporal Logic" featured in Philly Inquirer
July 24, 2019

Philly Inquirer article on Uber Elevate quotes our "Fly-by-Logic" research.


Konstantinos Mamouras & Arjun Radhakrishna gave talks at PLDI 2019
June 30, 2019

Two of Rajeev Alur's doctoral students, Konstantinos Mamouras (now at Rice) and Arjun Radhakrishna (now with Microsoft), presented their work at PLDI 2019.  

Links to their papers:

Arun Iyer, Manohar Jonnalagedda, Suresh Parthasarathy, Arjun Radhakrishna, Sriram K. Rajamani: Synthesis and Machine Learning for Heterogeneous Extraction.

Konstantinos Mamouras, Caleb Stanford, Rajeev Alur, Zachary G. Ives, Val Tannen: Data-Trace Types for Distributed Stream Processing Systems.

Mayur Naik & his team won Distinguished Paper Award at PLDI 2019
June 30, 2019

Kihong Heo, Mukund Raghothaman (soon to join USC CS), Xujie Si, and Mayur Naik are the recipients of the Distinguished Paper Award at the Conference on Programming Language Design and Implementation (PLDI 2019) for their paper "Continuously Reasoning about Programs using Differential Bayesian Inference".  Their abstract could be found at

Software developers are struggling to manage the rapidly growing size and complexity of the systems they develop, and are increasingly looking to sophisticated automatic techniques to help them improve the quality of their code. Static analysis is one such popular technique, and promises to automatically find bugs in software before it is even run. Recent years have witnessed the widespread adoption of static analysis tools by industry, from aerospace and safety-critical medical applications to security-conscious cloud service providers.  Unfortunately, the thoroughness of static analyzers is a double-edged sword, and developers are often overwhelmed by the number of warnings produced by tools. In their paper, Dr. Naik, with his postdocs Kihong Heo and Mukund Raghothaman, and his Ph.D.c Xujie Si, developed an AI-based system to prioritize these alarms based on how relevant they are to the developers’ immediate changes. Their system, Drake, will be more effective at identifying vulnerabilities, and promises to eliminate defects as soon as they are introduced into the code-base.  Our PRECISE team plans on deploying Drake on commercial software hosting services such as GitHub, in the coming months.


Linh Thi Xuan Phan appointed Co-Director of the Data Science Master's program
May 28, 2019

Linh Thi Xuan Phan has been appointed the co-director of the Data Science (DATS) Master's program. 

Linh is widely known as a dedicated teacher and someone highly engaged with master's students in education and research.  Many DATS students are taking her popular and highly-rated CIS 505, which covers topics related to big data infrastructures and cloud computing. She will add new dimensions to the program, given her expertise in big data infrastructures, cloud computing, and enhance DATS connections to embedded (health) device data analytics.

Congratulations, Linh!

Linh Thi Xuan Phan and her team won Best Paper Awards at the 25th IEEE RTAS 2019
April 22, 2019

Meng Xu, Linh Thi Xuan Phan, and Hyon-Young Choi (University of Pennsylvania); Yuhan Lin (Northeastern University); Haoran Li and Chenyang Lu (Washington University in St. Louis); and Insup Lee (University of Pennsylvania) are the recipients of the Best Paper Award at the 25th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), part of the Cyber-Physical Systems Week (CPSWeek), that took place in Montreal, Canada on 15-18 April 2019.  Their paper titled Holistic Resource Allocation for Multicore Real-Time Systems presents a holistic cache and memory bandwidth resource allocation strategy for multicore real-time systems.  Their strategy exploits the relationship between the allocation of cache and memory bandwidth resources and a task's WCET to map tasks onto cores and to compute the resource allocation for each core, to fully utilize resources while ensuring timing guarantees.  Extensive evaluations using real-world benchmarks show that their strategy offers near optimal schedulability performance while being highly efficient, and that it substantially outperforms state-of-the-art solutions.

Linh, and her former/current doctoral students (Saeed Abedi, Neeraj Gandhi, Henri Maxime Demoulin, Yang Li, and Yang Wu), also won RTAS Best Student Paper Award.  Their paper titled “RTNF: Predictable Latency for Network Function Virtualization” presents a scalable framework for the online resource allocation and scheduling of NFV applications that provides predictable end-to-end latency guarantees.  RTNF is based on a novel time-aware abstraction algorithm that transforms complex NFV graphs and their performance requirements into sets of scheduling interfaces; these can then be used by the resource manager and the scheduler on each node to efficiently allocate resources and to schedule NFV requests at runtime.  Their evaluation, based on simulations and an experimental prototype, shows that RTNF can schedule DAG-based NFV applications with solid timing guarantees while incurring only a small overhead, and that it substantially outperforms state-of-the-art  techniques.

Congratulations to all!

PRECISE releases Verisig v0.9 on GitHub
April 14, 2019

Verisig is a tool for verifying properties of neural networks in autonomous systems.  The novelty of Verisig lies in its encoding of a deep neural networks as hybrid systems such that it can be easily composed with hybrid systems models of vehicle dynamics and verified using state-of-the-art solvers (e.g., Flow*).  Consequently, Verisig has been used to verify safety properties of learning-enabled closed-loop controllers containing neural networks with 10s of layers and 100s of neurons per layer.  Verisig 0.9 represents the first public release of the tool, being actively developed as part of the DARPA Assured Autonomy program.

PRECISE's STEM Outreach: Empowering Girls to Learn About Cybersecurity, Technology, & Electronics
March 9, 2019

Cyberjutsu Girls (@CyberjutsuGirls) tweeted at 1:19 PM on Sat, Mar 09, 2019:
Today we're learning how cyber & medicine overlap in a new biomedical workshop: "Music from the Heart!" Our ladies are using @adafruit Huzzah to monitor heart rates & compete in a "rock band challenge" to see who can control them! Thanks to @IoMTprof for instructing! #GirlsInSTEM

Insup Lee named Deans' Distinguished Visiting Professor
January 24, 2019

The Deans' Distinguished Visiting Professorship is award to Insup Lee, Ph.D. by Perelman School of Medicine at the University of Pennsylvania on 17 Jan 2019. Dr. Lee presented to the audience a talk entitled "Internet of Medical Things (IoMT)" that day.

Deans Distinguished Visiting Professorship