callback( { "result":{ "query":":facetid:toc:\"db/conf/spin/spin2017.bht\"", "status":{ "@code":"200", "text":"OK" }, "time":{ "@unit":"msecs", "text":"196.03" }, "completions":{ "@total":"1", "@computed":"1", "@sent":"1", "c":{ "@sc":"26", "@dc":"26", "@oc":"26", "@id":"43414295", "text":":facetid:toc:db/conf/spin/spin2017.bht" } }, "hits":{ "@total":"26", "@computed":"26", "@sent":"26", "@first":"0", "hit":[{ "@score":"1", "@id":"3018318", "info":{"authors":{"author":{"@pid":"60/3666","text":"Domagoj Babic"}},"title":"SunDew: systematic automated security testing (keynote).","venue":"SPIN","pages":"10","year":"2017","type":"Conference and Workshop Papers","access":"closed","key":"conf/spin/Babic17","doi":"10.1145/3092282.3092314","ee":"https://doi.org/10.1145/3092282.3092314","url":"https://dblp.org/rec/conf/spin/Babic17"}, "url":"URL#3018318" }, { "@score":"1", "@id":"3018319", "info":{"authors":{"author":[{"@pid":"93/7218","text":"Marcello M. Bersani"},{"@pid":"183/4326","text":"Francesco Marconi"},{"@pid":"306/0008","text":"Matteo Rossi 0001"},{"@pid":"16/9868","text":"Madalina Erascu"},{"@pid":"39/922","text":"Silvio Ghilardi"}]},"title":"Formal verification of data-intensive applications through model checking modulo theories.","venue":"SPIN","pages":"98-101","year":"2017","type":"Conference and Workshop Papers","access":"closed","key":"conf/spin/BersaniMREG17","doi":"10.1145/3092282.3092300","ee":"https://doi.org/10.1145/3092282.3092300","url":"https://dblp.org/rec/conf/spin/BersaniMREG17"}, "url":"URL#3018319" }, { "@score":"1", "@id":"3018320", "info":{"authors":{"author":[{"@pid":"175/6602","text":"Vincent Bloemen"},{"@pid":"43/6032","text":"Alexandre Duret-Lutz"},{"@pid":"p/JvdPol","text":"Jaco van de Pol"}]},"title":"Explicit state model checking with generalized Büchi and Rabin automata.","venue":"SPIN","pages":"50-59","year":"2017","type":"Conference and Workshop Papers","access":"closed","key":"conf/spin/BloemenDP17","doi":"10.1145/3092282.3092288","ee":"https://doi.org/10.1145/3092282.3092288","url":"https://dblp.org/rec/conf/spin/BloemenDP17"}, "url":"URL#3018320" }, { "@score":"1", "@id":"3018321", "info":{"authors":{"author":[{"@pid":"193/3275","text":"Heila Botha"},{"@pid":"88/4695","text":"Oksana Tkachuk"},{"@pid":"59/6051","text":"Brink van der Merwe"},{"@pid":"54/5019","text":"Willem Visser"}]},"title":"Addressing challenges in obtaining high coverage when model checking Android applications.","venue":"SPIN","pages":"31-40","year":"2017","type":"Conference and Workshop Papers","access":"closed","key":"conf/spin/BothaTMV17","doi":"10.1145/3092282.3092302","ee":"https://doi.org/10.1145/3092282.3092302","url":"https://dblp.org/rec/conf/spin/BothaTMV17"}, "url":"URL#3018321" }, { "@score":"1", "@id":"3018322", "info":{"authors":{"author":{"@pid":"36/113","text":"Byron Cook"}},"title":"Automated formal reasoning about amazon web services (keynote).","venue":"SPIN","pages":"9","year":"2017","type":"Conference and Workshop Papers","access":"closed","key":"conf/spin/Cook17","doi":"10.1145/3092282.3092315","ee":"https://doi.org/10.1145/3092282.3092315","url":"https://dblp.org/rec/conf/spin/Cook17"}, "url":"URL#3018322" }, { "@score":"1", "@id":"3018323", "info":{"authors":{"author":[{"@pid":"191/3114","text":"Nima Dini"},{"@pid":"204/3692","text":"Cagdas Yelen"},{"@pid":"k/SarfrazKhurshid","text":"Sarfraz Khurshid"}]},"title":"Optimizing parallel Korat using invalid ranges.","venue":"SPIN","pages":"182-191","year":"2017","type":"Conference and Workshop Papers","access":"closed","key":"conf/spin/DiniYK17","doi":"10.1145/3092282.3092293","ee":"https://doi.org/10.1145/3092282.3092293","url":"https://dblp.org/rec/conf/spin/DiniYK17"}, "url":"URL#3018323" }, { "@score":"1", "@id":"3018324", "info":{"authors":{"author":[{"@pid":"18/7412","text":"John Fearnley"},{"@pid":"j/SanjayJain1","text":"Sanjay Jain 0001"},{"@pid":"38/5198","text":"Sven Schewe"},{"@pid":"s/FrankStephan","text":"Frank Stephan 0001"},{"@pid":"76/3220","text":"Dominik Wojtczak"}]},"title":"An ordered approach to solving parity games in quasi polynomial time and quasi linear space.","venue":"SPIN","pages":"112-121","year":"2017","type":"Conference and Workshop Papers","access":"closed","key":"conf/spin/FearnleyJS0W17","doi":"10.1145/3092282.3092286","ee":"https://doi.org/10.1145/3092282.3092286","url":"https://dblp.org/rec/conf/spin/FearnleyJS0W17"}, "url":"URL#3018324" }, { "@score":"1", "@id":"3018325", "info":{"authors":{"author":[{"@pid":"59/7272","text":"Marco A. Feliú"},{"@pid":"56/2819","text":"Camilo Rocha"},{"@pid":"204/3636","text":"Swee Balachandran"}]},"title":"Verification-driven development of ICAROUS based on automatic reachability analysis: a preliminary case study.","venue":"SPIN","pages":"94-97","year":"2017","type":"Conference and Workshop Papers","access":"closed","key":"conf/spin/FeliuRB17","doi":"10.1145/3092282.3120995","ee":"https://doi.org/10.1145/3092282.3120995","url":"https://dblp.org/rec/conf/spin/FeliuRB17"}, "url":"URL#3018325" }, { "@score":"1", "@id":"3018326", "info":{"authors":{"author":[{"@pid":"150/7924","text":"Paul Fiterau-Brostean"},{"@pid":"30/3515","text":"Toon Lenaerts"},{"@pid":"p/ErikPoll","text":"Erik Poll"},{"@pid":"24/10823","text":"Joeri de Ruiter"},{"@pid":"v/FritsWVaandrager","text":"Frits W. Vaandrager"},{"@pid":"204/3606","text":"Patrick Verleg"}]},"title":"Model learning and model checking of SSH implementations.","venue":"SPIN","pages":"142-151","year":"2017","type":"Conference and Workshop Papers","access":"closed","key":"conf/spin/Fiterau-Brostean17","doi":"10.1145/3092282.3092289","ee":"https://doi.org/10.1145/3092282.3092289","url":"https://dblp.org/rec/conf/spin/Fiterau-Brostean17"}, "url":"URL#3018326" }, { "@score":"1", "@id":"3018327", "info":{"authors":{"author":[{"@pid":"183/6426","text":"Thomas Geffroy"},{"@pid":"50/3164","text":"Jérôme Leroux"},{"@pid":"58/953","text":"Grégoire Sutre"}]},"title":"Backward coverability with pruning for lossy channel systems.","venue":"SPIN","pages":"132-141","year":"2017","type":"Conference and Workshop Papers","access":"closed","key":"conf/spin/GeffroyLS17","doi":"10.1145/3092282.3092292","ee":"https://doi.org/10.1145/3092282.3092292","url":"https://dblp.org/rec/conf/spin/GeffroyLS17"}, "url":"URL#3018327" }, { "@score":"1", "@id":"3018328", "info":{"authors":{"author":{"@pid":"h/GerardJHolzmann","text":"Gerard J. Holzmann"}},"title":"Cobra: fast structural code checking (keynote).","venue":"SPIN","pages":"1-8","year":"2017","type":"Conference and Workshop Papers","access":"closed","key":"conf/spin/Holzmann17","doi":"10.1145/3092282.3092313","ee":"https://doi.org/10.1145/3092282.3092313","url":"https://dblp.org/rec/conf/spin/Holzmann17"}, "url":"URL#3018328" }, { "@score":"1", "@id":"3018329", "info":{"authors":{"author":[{"@pid":"187/1596","text":"Jinru Hua"},{"@pid":"k/SarfrazKhurshid","text":"Sarfraz Khurshid"}]},"title":"EdSketch: execution-driven sketching for Java.","venue":"SPIN","pages":"162-171","year":"2017","type":"Conference and Workshop Papers","access":"closed","key":"conf/spin/HuaK17","doi":"10.1145/3092282.3092285","ee":"https://doi.org/10.1145/3092282.3092285","url":"https://dblp.org/rec/conf/spin/HuaK17"}, "url":"URL#3018329" }, { "@score":"1", "@id":"3018330", "info":{"authors":{"author":[{"@pid":"181/7731","text":"Idress Husien"},{"@pid":"65/9419","text":"Nicolas Berthier"},{"@pid":"38/5198","text":"Sven Schewe"}]},"title":"A hot method for synthesising cool controllers.","venue":"SPIN","pages":"122-131","year":"2017","type":"Conference and Workshop Papers","access":"closed","key":"conf/spin/HusienBS17","doi":"10.1145/3092282.3092299","ee":"https://doi.org/10.1145/3092282.3092299","url":"https://dblp.org/rec/conf/spin/HusienBS17"}, "url":"URL#3018330" }, { "@score":"1", "@id":"3018331", "info":{"authors":{"author":[{"@pid":"174/1426","text":"Marc Jasper"},{"@pid":"204/3671","text":"Maximilian Fecke"},{"@pid":"s/BernhardSteffen","text":"Bernhard Steffen"},{"@pid":"69/3212","text":"Markus Schordan"},{"@pid":"153/2465","text":"Jeroen Meijer"},{"@pid":"p/JvdPol","text":"Jaco van de Pol"},{"@pid":"12/8669","text":"Falk Howar"},{"@pid":"50/540","text":"Stephen F. Siegel"}]},"title":"The RERS 2017 challenge and workshop (invited paper).","venue":"SPIN","pages":"11-20","year":"2017","type":"Conference and Workshop Papers","access":"closed","key":"conf/spin/JasperFSSMPHS17","doi":"10.1145/3092282.3098206","ee":"https://doi.org/10.1145/3092282.3098206","url":"https://dblp.org/rec/conf/spin/JasperFSSMPHS17"}, "url":"URL#3018331" }, { "@score":"1", "@id":"3018332", "info":{"authors":{"author":[{"@pid":"204/3706","text":"Michalis Kokologiannakis"},{"@pid":"s/KonstantinosFSagonas","text":"Konstantinos Sagonas"}]},"title":"Stateless model checking of the Linux kernel's hierarchical read-copy-update (tree RCU).","venue":"SPIN","pages":"172-181","year":"2017","type":"Conference and Workshop Papers","access":"closed","key":"conf/spin/Kokologiannakis17","doi":"10.1145/3092282.3092287","ee":"https://doi.org/10.1145/3092282.3092287","url":"https://dblp.org/rec/conf/spin/Kokologiannakis17"}, "url":"URL#3018332" }, { "@score":"1", "@id":"3018333", "info":{"authors":{"author":[{"@pid":"93/5951","text":"Guangyuan Li"},{"@pid":"144/4964","text":"Peter Gjøl Jensen"},{"@pid":"l/KimGuldstrandLarsen","text":"Kim Guldstrand Larsen"},{"@pid":"52/579","text":"Axel Legay"},{"@pid":"84/9829","text":"Danny Bøgsted Poulsen"}]},"title":"Practical controller synthesis for MTL0, ∞.","venue":"SPIN","pages":"102-111","year":"2017","type":"Conference and Workshop Papers","access":"closed","key":"conf/spin/LiJLLP17","doi":"10.1145/3092282.3092303","ee":"https://doi.org/10.1145/3092282.3092303","url":"https://dblp.org/rec/conf/spin/LiJLLP17"}, "url":"URL#3018333" }, { "@score":"1", "@id":"3018334", "info":{"authors":{"author":[{"@pid":"204/3658","text":"Blake Loring"},{"@pid":"204/3748","text":"Duncan Mitchell"},{"@pid":"74/3780","text":"Johannes Kinder"}]},"title":"ExpoSE: practical symbolic execution of standalone JavaScript.","venue":"SPIN","pages":"196-199","year":"2017","type":"Conference and Workshop Papers","access":"closed","key":"conf/spin/LoringMK17","doi":"10.1145/3092282.3092295","ee":"https://doi.org/10.1145/3092282.3092295","url":"https://dblp.org/rec/conf/spin/LoringMK17"}, "url":"URL#3018334" }, { "@score":"1", "@id":"3018335", "info":{"authors":{"author":[{"@pid":"204/3662","text":"Pouria Mellati"},{"@pid":"99/7840","text":"Ehsan Khamespanah"},{"@pid":"93/1066","text":"Ramtin Khosravi"}]},"title":"LeeTL: LTL with quantifications over model objects.","venue":"SPIN","pages":"41-49","year":"2017","type":"Conference and Workshop Papers","access":"closed","key":"conf/spin/MellatiKK17","doi":"10.1145/3092282.3092294","ee":"https://doi.org/10.1145/3092282.3092294","url":"https://dblp.org/rec/conf/spin/MellatiKK17"}, "url":"URL#3018335" }, { "@score":"1", "@id":"3018336", "info":{"authors":{"author":[{"@pid":"153/2596","text":"Huu-Vu Nguyen"},{"@pid":"23/6190","text":"Tayssir Touili"}]},"title":"CARET model checking for malware detection.","venue":"SPIN","pages":"152-161","year":"2017","type":"Conference and Workshop Papers","access":"closed","key":"conf/spin/NguyenT17","doi":"10.1145/3092282.3092301","ee":"https://doi.org/10.1145/3092282.3092301","url":"https://dblp.org/rec/conf/spin/NguyenT17"}, "url":"URL#3018336" }, { "@score":"1", "@id":"3018337", "info":{"authors":{"author":[{"@pid":"178/0425","text":"Wytse Oortwijn"},{"@pid":"126/8210","text":"Tom van Dijk"},{"@pid":"p/JvdPol","text":"Jaco van de Pol"}]},"title":"Distributed binary decision diagrams for symbolic reachability.","venue":"SPIN","pages":"21-30","year":"2017","type":"Conference and Workshop Papers","access":"closed","key":"conf/spin/OortwijnDP17","doi":"10.1145/3092282.3092284","ee":"https://doi.org/10.1145/3092282.3092284","url":"https://dblp.org/rec/conf/spin/OortwijnDP17"}, "url":"URL#3018337" }, { "@score":"1", "@id":"3018338", "info":{"authors":{"author":[{"@pid":"13/4540","text":"Laura Panizo"},{"@pid":"58/5850","text":"Alberto Salmerón"},{"@pid":"15/4377","text":"María-del-Mar Gallardo"},{"@pid":"95/1885","text":"Pedro Merino 0001"}]},"title":"Guided test case generation for mobile apps in the TRIANGLE project: work in progress.","venue":"SPIN","pages":"192-195","year":"2017","type":"Conference and Workshop Papers","access":"closed","key":"conf/spin/PanizoSG017","doi":"10.1145/3092282.3092298","ee":"https://doi.org/10.1145/3092282.3092298","url":"https://dblp.org/rec/conf/spin/PanizoSG017"}, "url":"URL#3018338" }, { "@score":"1", "@id":"3018339", "info":{"authors":{"author":[{"@pid":"125/1160","text":"Srinivas Pinisetty"},{"@pid":"r/ParthaSRoop","text":"Partha S. Roop"},{"@pid":"145/1000","text":"Steven Smyth"},{"@pid":"85/6852","text":"Stavros Tripakis"},{"@pid":"17/1867","text":"Reinhard von Hanxleden"}]},"title":"Runtime enforcement of reactive systems using synchronous enforcers.","venue":"SPIN","pages":"80-89","year":"2017","type":"Conference and Workshop Papers","access":"closed","key":"conf/spin/PinisettyRSTH17","doi":"10.1145/3092282.3092291","ee":"https://doi.org/10.1145/3092282.3092291","url":"https://dblp.org/rec/conf/spin/PinisettyRSTH17"}, "url":"URL#3018339" }, { "@score":"1", "@id":"3018340", "info":{"authors":{"author":[{"@pid":"60/4196","text":"Daniel Ratiu"},{"@pid":"04/7011","text":"Andreas Ulrich"}]},"title":"Increasing usability of spin-based C code verification using a harness definition language: leveraging model-driven code checking to practitioners.","venue":"SPIN","pages":"60-69","year":"2017","type":"Conference and Workshop Papers","access":"closed","key":"conf/spin/RatiuU17","doi":"10.1145/3092282.3092283","ee":"https://doi.org/10.1145/3092282.3092283","url":"https://dblp.org/rec/conf/spin/RatiuU17"}, "url":"URL#3018340" }, { "@score":"1", "@id":"3018341", "info":{"authors":{"author":[{"@pid":"169/1158","text":"Matthieu Renard"},{"@pid":"r/AntoineRollet","text":"Antoine Rollet"},{"@pid":"11/5986","text":"Yliès Falcone"}]},"title":"Runtime enforcement using Büchi games.","venue":"SPIN","pages":"70-79","year":"2017","type":"Conference and Workshop Papers","access":"closed","key":"conf/spin/RenardRF17","doi":"10.1145/3092282.3092296","ee":"https://doi.org/10.1145/3092282.3092296","url":"https://dblp.org/rec/conf/spin/RenardRF17"}, "url":"URL#3018341" }, { "@score":"1", "@id":"3018342", "info":{"authors":{"author":[{"@pid":"94/7566","text":"Lucas G. Wagner"},{"@pid":"03/3829","text":"David A. Greve"},{"@pid":"84/6151","text":"Andrew Gacek"}]},"title":"SIMPAL: a compositional reasoning framework for imperative programs.","venue":"SPIN","pages":"90-93","year":"2017","type":"Conference and Workshop Papers","access":"closed","key":"conf/spin/WagnerGG17","doi":"10.1145/3092282.3092290","ee":"https://doi.org/10.1145/3092282.3092290","url":"https://dblp.org/rec/conf/spin/WagnerGG17"}, "url":"URL#3018342" }, { "@score":"1", "@id":"3036449", "info":{"authors":{"author":[{"@pid":"e/HakanErdogmus","text":"Hakan Erdogmus"},{"@pid":"84/3029","text":"Klaus Havelund"}]},"title":"Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, Santa Barbara, CA, USA, July 10-14, 2017","venue":"SPIN","publisher":"ACM","year":"2017","type":"Editorship","key":"conf/spin/2017","ee":"http://dl.acm.org/citation.cfm?id=3092282","url":"https://dblp.org/rec/conf/spin/2017"}, "url":"URL#3036449" } ] } } } )