Write a Blog >>
SPIN 2017
Thu 13 - Fri 14 July 2017
Santa Barbara, California, United States
co-located with
ISSTA 2017
Toggle navigation
Attending
Venue: University of California, Santa Barbara
Registration and Accommodations
Visas and Travel
Program
SPIN Program
Your Program
Call for Papers
Accepted Papers
Keynote Speakers
Proceedings
Thu 13 Jul
Fri 14 Jul
Tracks
SPIN 2017
SPIN Agenda
SPIN Keynote
SPIN Full Paper
SPIN Short Paper
RERS
Organization
SPIN 2017 Committees
Organizing Committee
Steering Committee
Program Committee
Contributors
People Index
Search
Series
Series
SPIN 2021
SPIN 2019
SPIN 2017
Sign in
Sign up
ISSTA 2017
(
series
) /
SPIN 2017
(
series
) /
University of California, Santa Barbara
/
Room information: ESB 1001
Venue
University of California, Santa Barbara
Room name
ESB 1001
Floor
1
Room number
1001
Room Information
No extra information available
Program
Detailed Table
Session Timeline
Detailed Timeline
Program Display Configuration
Time Zone
The program is currently displayed in
(GMT-07:00) Tijuana, Baja California
.
Use conference time zone: (GMT-07:00) Tijuana, Baja California
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-09:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-08:00) Alaska
(GMT-07:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-07:00) Pacific Time (US & Canada)
(GMT-06:00) Mountain Time (US & Canada)
(GMT-06:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-05:00) Guadalajara, Mexico City, Monterrey
(GMT-06:00) Easter Island
(GMT-05:00) Central Time (US & Canada)
(GMT-04:00) Eastern Time (US & Canada)
(GMT-04:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-04:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-04:00) Manaus, Amazonas, Brazil
(GMT-03:00) Atlantic Time (Goose Bay)
(GMT-03:00) Atlantic Time (Canada)
(GMT-02:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-02:00) Miquelon, St. Pierre
(GMT-02:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-03:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT) Azores
(UTC) Coordinated Universal Time
(GMT+01:00) Belfast
(GMT+01:00) Dublin
(GMT+01:00) Lisbon
(GMT+01:00) London
(GMT) Monrovia, Reykjavik
(GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+02:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+02:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+01:00) Windhoek
(GMT+03:00) Athens
(GMT+03:00) Beirut
(GMT+02:00) Cairo
(GMT+03:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+03:00) Jerusalem
(GMT+03:00) Minsk
(GMT+03:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+04:30) Tehran
(GMT+04:00) Abu Dhabi, Muscat
(GMT+04:00) Yerevan
(GMT+04:30) Kabul
(GMT+05:00) Ekaterinburg
(GMT+05:00) Tashkent
(GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi
(GMT+05:45) Kathmandu
(GMT+06:00) Astana, Dhaka
(GMT+07:00) Novosibirsk
(GMT+06:30) Yangon (Rangoon)
(GMT+07:00) Bangkok, Hanoi, Jakarta
(GMT+07:00) Krasnoyarsk
(GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi
(GMT+08:00) Irkutsk, Ulaan Bataar
(GMT+08:00) Perth
(GMT+08:45) Eucla
(GMT+09:00) Osaka, Sapporo, Tokyo
(GMT+09:00) Seoul
(GMT+09:00) Yakutsk
(GMT+09:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+10:00) Hobart
(GMT+10:00) Vladivostok
(GMT+10:30) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+11:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+12:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+12:45) Chatham Islands
(GMT+13:00) Nuku'alofa
(GMT+14:00) Kiritimati
The GMT offsets shown reflect the offsets
at the moment of the conference
.
Time Band
By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.
Display full program
Specify a time band
-
Save
×
You're viewing the program in a time zone which is different from your device's time zone
change time zone
Thu 13 Jul
Displayed time zone:
Tijuana, Baja California
change
08:30 - 09:30
Session 1
SPIN Keynote
at
ESB 1001
Chair(s):
Hakan Erdogmus
Carnegie Mellon University
,
Klaus Havelund
NASA/Caltech Jet Propulsion Laboratory
08:30
60m
Talk
Gerard Holzmann: Cobra - Fast Structural Code Checking
SPIN Keynote
09:30 - 10:00
Session 2: Symbolic Verification
SPIN Full Paper
at
ESB 1001
Chair(s):
Klaus Havelund
NASA/Caltech Jet Propulsion Laboratory
09:30
30m
Talk
Distributed Binary Decision Diagrams for Symbolic Reachability (Wytse Oortwijn, Tom van Dijk and Jaco van de Pol)
SPIN Full Paper
10:30 - 12:00
Session 3: Model Checking
SPIN Full Paper
at
ESB 1001
Chair(s):
Neha Rungta
Amazon Web Services
10:30
30m
Talk
Addressing Challenges In Obtaining High Coverage When Model Checking Android Applications (Heila Botha, Oksana Tkachuk, Brink Van Der Merwe and Willem Visser)
SPIN Full Paper
11:00
30m
Talk
LeeTL: LTL with Quantifications Over Model Objects (Pouria Mellati, Ehsan Khamespanah and Ramtin Khosravi)
SPIN Full Paper
11:30
30m
Talk
Explicit State Model Checking with Generalized Büchi and Rabin Automata (Vincent Bloemen, Alexandre Duret-Lutz and Jaco van de Pol)
SPIN Full Paper
13:30 - 14:30
Session 4
SPIN Keynote
at
ESB 1001
Chair(s):
Klaus Havelund
NASA/Caltech Jet Propulsion Laboratory
13:30
60m
Talk
Byron Cook: Automated Formal Reasoning About Amazon Web Services
SPIN Keynote
14:30 - 15:00
Session 5: Code Verification
SPIN Full Paper
at
ESB 1001
Chair(s):
Alberto Salmeron
14:30
30m
Talk
Increasing Usability of Spin-based C Code Verification Using a Harness Definition Language (Daniel Ratiu and Andreas Ulrich)
SPIN Full Paper
15:30 - 16:30
Session 6: Runtime Enforcement
SPIN Full Paper
at
ESB 1001
Chair(s):
Axel Legay
15:30
30m
Talk
Runtime Enforcement Using Büchi Games (Matthieu Renard, Antoine Rollet and Ylies Falcone)
SPIN Full Paper
16:00
30m
Talk
Runtime Enforcement of Reactive Systems Using Synchronous Enforcers (Srinivas Pinisetty, Partha Roop, Steven Smyth, Stavros Tripakis and Reinhard von Hanxleden)
SPIN Full Paper
16:30 - 17:30
Session 7: Model Checking
SPIN Short Paper
at
ESB 1001
Chair(s):
Pedro Merino Gomez
16:30
20m
Talk
SIMPAL: A Compositional Reasoning Framework for Imperative Programs (Lucas Wagner, David Greve and Andrew Gacek)
SPIN Short Paper
16:50
20m
Talk
Verification-Driven Development of Icarous Based on Automatic Reachability Analysis (Marco Antonio Feliu Gabaldon, Camilo Rocha and Swee Balachandran)
SPIN Short Paper
17:10
20m
Talk
Formal Verification of Data-Intensive Applications through Model Checking Modulo Theories (Marcello M. Bersani, Madalina Erascu, Francesco Marconi, Silvio Ghilardi and Matteo Rossi)
SPIN Short Paper
Fri 14 Jul
Displayed time zone:
Tijuana, Baja California
change
08:30 - 10:00
Session 8: Program Synthesis
SPIN Full Paper
at
ESB 1001
Chair(s):
Stefan Leue
University of Konstanz
08:30
30m
Talk
Practical Controller Synthesis for MTL_{0,∞} (Guangyuan Li, Peter Gjøl Jensen, Kim Guldstrand Larsen, Axel Legay and Danny Bøgsted Poulsen)
SPIN Full Paper
09:00
30m
Talk
An Ordered Approach to Solving Parity Games in Quasi Polynomial Time and Quasi Linear Space (John Fearnley, Sanjay Jain, Sven Schewe, Frank Stephan and Dominik Wojtczak)
SPIN Full Paper
09:30
30m
Talk
A Hot Method for Synthesising Cool Controllers (Idress Husien, Nicolas Berthier and Sven Schewe)
SPIN Full Paper
10:30 - 12:00
Session 9: Model Checking
SPIN Full Paper
at
ESB 1001
Chair(s):
Konstantinos (Kostis) Sagonas
10:30
30m
Talk
Backward Coverability with Pruning for Lossy Channel Systems (Thomas Geffroy, Jérôme Leroux and Grégoire Sutre)
SPIN Full Paper
11:00
30m
Talk
Model Learning and Model Checking of SSH Implementations (Paul Fiterau-Brostean, Frits Vaandrager, Erik Poll, Joeri de Ruiter, Toon Lenaerts and Patrick Verleg)
SPIN Full Paper
11:30
30m
Talk
CARET Model Checking for Malware Detection (Huu Vu Nguyen and Tayssir Touili)
SPIN Full Paper
13:30 - 14:30
Session 10
SPIN Keynote
at
ESB 1001
Chair(s):
Yliès Falcone
Univ. Grenoble Alpes, Inria
13:30
60m
Talk
Domagoj Babic: SunDew - Systematic Automated Security Testing.
SPIN Keynote
14:30 - 15:00
Session 11: Program Sketching
SPIN Full Paper
at
ESB 1001
Chair(s):
Madalina Erascu
14:30
30m
Talk
EdSketch: Execution-Driven Sketching for Java (Jinru Hua and Sarfraz Khurshid)
SPIN Full Paper
15:30 - 16:30
Session 12: Testing
SPIN Full Paper
at
ESB 1001
Chair(s):
Jaco van de Pol
University of Twente
15:30
30m
Talk
Stateless Model Checking of the Linux Kernel's Hierarchical Read-Copy-Update (Tree RCU) (Michalis Kokologiannakis and Konstantinos Sagonas)
SPIN Full Paper
16:00
30m
Talk
Optimizing Parallel Korat Using Invalid Ranges (Nima Dini, Cagdas Yelen and Sarfraz Khurshid)
SPIN Full Paper
16:30 - 17:10
Session 13: Testing
SPIN Short Paper
at
ESB 1001
Chair(s):
Antoine Rollet
16:30
20m
Talk
Guided Test Case Generation for Mobile Apps in the TRIANGLE Project (Laura Panizo, Alberto Salmerón, Maria Del Mar Gallardo and Pedro Merino)
SPIN Short Paper
16:50
20m
Talk
ExpoSE: Practical Symbolic Execution of Standalone JavaScript (Blake Loring, Duncan Mitchell and Johannes Kinder)
SPIN Short Paper
17:10 - 17:30
Session 14
SPIN Agenda
at
ESB 1001
Chair(s):
Hakan Erdogmus
Carnegie Mellon University
,
Klaus Havelund
NASA/Caltech Jet Propulsion Laboratory
,
Pedro Merino Gomez
17:10
20m
Day closing
SPIN 2018, Best Paper Awards, and Closing
SPIN Agenda
Thu 13 Jul
Displayed time zone:
Tijuana, Baja California
change
Room
8:00
30
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
ESB 1001
SPIN Keynote
Session 1
SPIN Full Paper
Session 2: Symbolic Verification
SPIN Full Paper
Session 3: Model Checking
SPIN Keynote
Session 4
SPIN Full Paper
Session 5: Code Verification
SPIN Full Paper
Session 6: Runtime Enforcement
SPIN Short Paper
Session 7: Model Checking
Fri 14 Jul
Displayed time zone:
Tijuana, Baja California
change
Room
8:00
30
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
ESB 1001
SPIN Full Paper
Session 8: Program Synthesis
SPIN Full Paper
Session 9: Model Checking
SPIN Keynote
Session 10
SPIN Full Paper
Session 11: Program Sketching
SPIN Full Paper
Session 12: Testing
SPIN Short Paper
Session 13: Testing
SPIN Agenda
Session 14
Thu 13 Jul
Displayed time zone:
Tijuana, Baja California
change
Room
8:00
15
30
45
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
ESB 1001
SPIN Keynote
Gerard Holzmann: Cobra - Fast Structural Code Checking
08:30 - 09:30
SPIN Full Paper
Distributed Binary Decision Diagrams for Symbolic Reachability (Wytse O ...
09:30 - 10:00
SPIN Full Paper
Addressing Challenges In Obtaining High Coverage When Model Checking An ...
10:30 - 11:00
SPIN Full Paper
LeeTL: LTL with Quantifications Over Model Objects (Pouria Mellati, Eh ...
11:00 - 11:30
SPIN Full Paper
Explicit State Model Checking with Generalized Büchi and Rabin Automata ...
11:30 - 12:00
SPIN Keynote
Byron Cook: Automated Formal Reasoning About Amazon Web Services
13:30 - 14:30
SPIN Full Paper
Increasing Usability of Spin-based C Code Verification Using a Harness ...
14:30 - 15:00
SPIN Full Paper
Runtime Enforcement Using Büchi Games (Matthieu Renard, Antoine Rollet ...
15:30 - 16:00
SPIN Full Paper
Runtime Enforcement of Reactive Systems Using Synchronous Enforcers (Sr ...
16:00 - 16:30
SPIN Short Paper
SIMPAL: A Compositional Reasoning Framework for Imperative Programs (Lu ...
16:30 - 16:50
SPIN Short Paper
Verification-Driven Development of Icarous Based on Automatic Reachabil ...
16:50 - 17:10
SPIN Short Paper
Formal Verification of Data-Intensive Applications through Model Checki ...
17:10 - 17:30
Fri 14 Jul
Displayed time zone:
Tijuana, Baja California
change
Room
8:00
15
30
45
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
ESB 1001
SPIN Full Paper
Practical Controller Synthesis for MTL_{0,∞} (Guangyuan Li, Peter Gjøl ...
08:30 - 09:00
SPIN Full Paper
An Ordered Approach to Solving Parity Games in Quasi Polynomial Time an ...
09:00 - 09:30
SPIN Full Paper
A Hot Method for Synthesising Cool Controllers (Idress Husien, Nicolas ...
09:30 - 10:00
SPIN Full Paper
Backward Coverability with Pruning for Lossy Channel Systems (Thomas Ge ...
10:30 - 11:00
SPIN Full Paper
Model Learning and Model Checking of SSH Implementations (Paul Fiterau- ...
11:00 - 11:30
SPIN Full Paper
CARET Model Checking for Malware Detection (Huu Vu Nguyen and Tayssir T ...
11:30 - 12:00
SPIN Keynote
Domagoj Babic: SunDew - Systematic Automated Security Testing.
13:30 - 14:30
SPIN Full Paper
EdSketch: Execution-Driven Sketching for Java (Jinru Hua and Sarfraz Kh ...
14:30 - 15:00
SPIN Full Paper
Stateless Model Checking of the Linux Kernel's Hierarchical Read-Copy-U ...
15:30 - 16:00
SPIN Full Paper
Optimizing Parallel Korat Using Invalid Ranges (Nima Dini, Cagdas Yelen ...
16:00 - 16:30
SPIN Short Paper
Guided Test Case Generation for Mobile Apps in the TRIANGLE Project (La ...
16:30 - 16:50
SPIN Short Paper
ExpoSE: Practical Symbolic Execution of Standalone JavaScript (Blake Lo ...
16:50 - 17:10
SPIN Agenda
SPIN 2018, Best Paper Awards, and Closing
17:10 - 17:30
x
Thu 21 Nov 14:49