Program

08:30 Breakfast and Gathering
Breakfast: bagels, muffins, pastry, coffee, tea.
09:00 Invited Talk
Matt Might, University of Utah
AAM for AAM: Analyzing Android for Malware by Abstracting Abstract Machines
10:00 Coffee Break
10:30 Symbolic Execution
  • Justin Lloyd and Elena Sherman. Minimizing the Size of Path Conditions Using Convex Polyhedra Abstract Domain
  • Jaideep Ramachandran, Corina Pasareanu and Thomas Wahl. Symbolic Execution for Checking the Accuracy of Floating-Point Programs
  • Marko Dimjasevic, Dimitra Giannakopoulou, Falk Howar, Malte Isberner, Zvonimir Rakamaric and Vishwanath Raman. The Dart, the Psyco, and the Doop
  • Stuart Siroky, Rodion Podorozhny and Guowei Yang. Verification of Architectural Constraints on Sequences of Method Invocations
12:00 Lunch
Check out our suggested lunch options nearby. Please don't be late for student poster session.
13:30 Student Poster Session
14:30 Testing and Android
  • Daniel Bryce and Renee Bryce. Combinatorial Branchcounting in Java PathFinder
  • Simone Hanazumi, Ana De Melo and Corina Pasareanu. From Testing Purposes to Formal JPF Properties
  • Rody Kersten, Suzette Person, Neha Rungta and Oksana Tkachuk. Improving Coverage of Test-Cases Generated by Symbolic Pathfinder for Programs with Loops
  • Heila van der Merwe, Oksana Tkachuk, Brink van der Merwe and Willem Visser. Generation of Library Models for Verification of Android Applications
16:00 Coffee Break
16:30 Concurrency and Type Checking
  • Peter Anderson and Eric Mercer. JPF Verification of Habanero Java Programs using Gradual Type Permission Regions
  • Quoc-Sang Phan, Pasquale Malacaria and Corina Pasareanu. Concurrent Bounded Model Checking
  • Kelvin Nilsen. Combining Static Analysis with Enhanced Type Checking in Safety-Critical Java
17:30 Break
17:45 Open Business Meeting
Topics: jpf.byu.edu and jpf-core release cycle, Java 8, JPF-workshop 2015
19:00 Dinner
Taqueria 27, Foothill Drive location