Mon 5 Nov 2018 14:30 - 15:00 at Spring Lake - JPF Workshop

Software systems are often shipped and deployed with both known and unknown bugs. On-the-fly program repairs, which handle runtime errors and allow programs to continue successfully, can help software reliability, e.g., by dealing with inconsistent or corrupted data without interrupting the running program. We report on our work-in-progress that repairs data structure using separation logic. Our technique, inspired by existing works on specification-based repair, takes as input a specification written in a separation logic formula and a concrete data structure that fails that specification, and performs on-the-fly repair to make the data conforms with the specification. The use of separation logic allows us to compactly and precisely represent desired properties of data structures and use existing analyses in separation logic to detect and repair bugs in complex data structures. We have developed a prototype, called STARFIX, to repair invalid Java data structures violating given specifications in separation logic. Preliminary results show that tool can efficiently detect and repair inconsistent data structures including lists and trees.

Mon 5 Nov

Displayed time zone: Guadalajara, Mexico City, Monterrey change

08:30 - 17:00
JPF WorkshopJPF at Spring Lake
09:00
10m
Day opening
Opening
JPF

09:10
50m
Talk
Keynote: Side-Channel Analysis via Symbolic Execution and Model Counting
JPF
Tevfik Bultan University of California, Santa Barbara
10:00
30m
Coffee break
Coffee break
JPF

10:30
30m
Research paper
Assessing the Adequacy of Synthetic Programs for Learning SPF's Configurations
JPF
Maria Paquin Boise State University, Elena Sherman Boise State University, Amit Jain Boise State University
11:00
30m
Research paper
Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP)
JPF
Lucas C. Cordeiro University of Manchester, UK, Daniel Kroening University of Oxford, Peter Schrammel University of Sussex
11:30
30m
Research paper
Attack Synthesis for Strings using Meta-Heuristics
JPF
Seemanta Saha University of California Santa Barbara, Ismet Burak Kadron University of California at Santa Barbara, USA, William Eiers University of California at Santa Barbara, USA, Lucas Bang , Tevfik Bultan University of California, Santa Barbara
12:00
90m
Lunch
Lunch @Lakeview Restaurant West
JPF

13:30
30m
Talk
Invited talk: Test input generation using separation logic
JPF
Quoc-Sang Phan Fujitsu Laboratories of America
14:00
30m
Research paper
Memory safety in C by abstract interpretation
JPF
joseph Jones Brigham Young University, James Wasson Brigham Young University, Sean Brown Brigham Young University, Seth Poulsen Brigham Young University, Peter Aldous Brigham Young University, Eric Mercer Brigham Young University
14:30
30m
Research paper
Automatic Data Structure Repair using Separation Logic
JPF
Guolong Zheng University of Nebraska Lincoln, Quang Loc Le School of Computing, Teesside University, UK, ThanhVu Nguyen University of Nebraska-Lincoln, Quoc-Sang Phan Fujitsu Laboratories of America
15:00
30m
Coffee break
Coffee break
JPF

15:30
30m
Research paper
A Progress Bar for the JPF Search Using Program Executions
JPF
Kaiyuan Wang , Hayes Converse The University of Texas at Austin, Milos Gligoric University of Texas at Austin, Sasa Misailovic University of Illinois at Urbana-Champaign, Sarfraz Khurshid University of Texas at Austin
16:00
50m
Meeting
JPF Open Discussion
JPF

16:50
10m
Day closing
Closing
JPF