callback( { "result":{ "query":":facetid:toc:\"db/conf/atva/atva2016.bht\"", "status":{ "@code":"200", "text":"OK" }, "time":{ "@unit":"msecs", "text":"65.65" }, "completions":{ "@total":"1", "@computed":"1", "@sent":"1", "c":{ "@sc":"33", "@dc":"33", "@oc":"33", "@id":"43380860", "text":":facetid:toc:db/conf/atva/atva2016.bht" } }, "hits":{ "@total":"33", "@computed":"33", "@sent":"30", "@first":"0", "hit":[{ "@score":"1", "@id":"3210853", "info":{"authors":{"author":[{"@pid":"32/8421-1","text":"Nils Jansen 0001"},{"@pid":"124/8982","text":"Christian Dehnert"},{"@pid":"39/9937","text":"Benjamin Lucien Kaminski"},{"@pid":"k/JoostPieterKatoen","text":"Joost-Pieter Katoen"},{"@pid":"180/5683-1","text":"Lukas Westhofen 0001"}]},"title":"Bounded Model Checking for Probabilistic Programs.","venue":"ATVA","pages":"68-85","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/0001DKKW16","doi":"10.1007/978-3-319-46520-3_5","ee":"https://doi.org/10.1007/978-3-319-46520-3_5","url":"https://dblp.org/rec/conf/atva/0001DKKW16"}, "url":"URL#3210853" }, { "@score":"1", "@id":"3210854", "info":{"authors":{"author":[{"@pid":"19/3904","text":"Alessandro Abate"},{"@pid":"213/3728","text":"Milan Ceska 0002"},{"@pid":"k/MartaZKwiatkowska","text":"Marta Kwiatkowska"}]},"title":"Approximate Policy Iteration for Markov Decision Processes via Quantitative Adaptive Aggregations.","venue":"ATVA","pages":"13-31","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/AbateCK16","doi":"10.1007/978-3-319-46520-3_2","ee":"https://doi.org/10.1007/978-3-319-46520-3_2","url":"https://dblp.org/rec/conf/atva/AbateCK16"}, "url":"URL#3210854" }, { "@score":"1", "@id":"3210855", "info":{"authors":{"author":[{"@pid":"22/10894","text":"Florent Avellaneda"},{"@pid":"20/5526","text":"Silvano Dal-Zilio"},{"@pid":"48/1501","text":"Jean-Baptiste Raclet"}]},"title":"Solving Language Equations Using Flanked Automata.","venue":"ATVA","pages":"106-121","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/AvellanedaDR16","doi":"10.1007/978-3-319-46520-3_7","ee":"https://doi.org/10.1007/978-3-319-46520-3_7","url":"https://dblp.org/rec/conf/atva/AvellanedaDR16"}, "url":"URL#3210855" }, { "@score":"1", "@id":"3210856", "info":{"authors":{"author":[{"@pid":"b/ChristelBaier","text":"Christel Baier"},{"@pid":"50/2079","text":"Sascha Klüppelholz"},{"@pid":"m/HermanndeMeer","text":"Hermann de Meer"},{"@pid":"49/7113","text":"Florian Niedermeier"},{"@pid":"143/2676","text":"Sascha Wunderlich"}]},"title":"Greener Bits: Formal Analysis of Demand Response.","venue":"ATVA","pages":"323-339","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/BaierKMNW16","doi":"10.1007/978-3-319-46520-3_21","ee":"https://doi.org/10.1007/978-3-319-46520-3_21","url":"https://dblp.org/rec/conf/atva/BaierKMNW16"}, "url":"URL#3210856" }, { "@score":"1", "@id":"3210857", "info":{"authors":{"author":[{"@pid":"46/3025","text":"Shoham Ben-David"},{"@pid":"c/MarshaChechik","text":"Marsha Chechik"},{"@pid":"21/1391","text":"Sebastián Uchitel"}]},"title":"Observational Refinement and Merge for Disjunctive MTSs.","venue":"ATVA","pages":"287-303","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/Ben-DavidCU16","doi":"10.1007/978-3-319-46520-3_19","ee":"https://doi.org/10.1007/978-3-319-46520-3_19","url":"https://dblp.org/rec/conf/atva/Ben-DavidCU16"}, "url":"URL#3210857" }, { "@score":"1", "@id":"3210858", "info":{"authors":{"author":[{"@pid":"71/1110","text":"Nikola Benes"},{"@pid":"92/3060","text":"Lubos Brim"},{"@pid":"167/4522","text":"Martin Demko"},{"@pid":"167/4487","text":"Samuel Pastva"},{"@pid":"86/2438","text":"David Safránek"}]},"title":"Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-affine Systems.","venue":"ATVA","pages":"192-208","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/BenesBDPS16","doi":"10.1007/978-3-319-46520-3_13","ee":"https://doi.org/10.1007/978-3-319-46520-3_13","url":"https://dblp.org/rec/conf/atva/BenesBDPS16"}, "url":"URL#3210858" }, { "@score":"1", "@id":"3210859", "info":{"authors":{"author":[{"@pid":"18/3197","text":"Tomás Brázdil"},{"@pid":"k/AntoninKucera","text":"Antonín Kucera 0001"},{"@pid":"91/10961","text":"Petr Novotný 0001"}]},"title":"Optimizing the Expected Mean Payoff in Energy Markov Decision Processes.","venue":"ATVA","pages":"32-49","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/BrazdilKN16","doi":"10.1007/978-3-319-46520-3_3","ee":"https://doi.org/10.1007/978-3-319-46520-3_3","url":"https://dblp.org/rec/conf/atva/BrazdilKN16"}, "url":"URL#3210859" }, { "@score":"1", "@id":"3210860", "info":{"authors":{"author":[{"@pid":"87/8371","text":"Romain Brenguier"},{"@pid":"01/2980","text":"Vojtech Forejt"}]},"title":"Decidability Results for Multi-objective Stochastic Games.","venue":"ATVA","pages":"227-243","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/BrenguierF16","doi":"10.1007/978-3-319-46520-3_15","ee":"https://doi.org/10.1007/978-3-319-46520-3_15","url":"https://dblp.org/rec/conf/atva/BrenguierF16"}, "url":"URL#3210860" }, { "@score":"1", "@id":"3210861", "info":{"authors":{"author":[{"@pid":"180/5404","text":"Pavel Cadek"},{"@pid":"37/1716","text":"Jan Strejcek"},{"@pid":"24/9889","text":"Marek Trtík"}]},"title":"Tighter Loop Bound Analysis.","venue":"ATVA","pages":"512-527","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/CadekST16","doi":"10.1007/978-3-319-46520-3_32","ee":"https://doi.org/10.1007/978-3-319-46520-3_32","url":"https://dblp.org/rec/conf/atva/CadekST16"}, "url":"URL#3210861" }, { "@score":"1", "@id":"3210862", "info":{"authors":{"author":[{"@pid":"187/1665","text":"David Deininger"},{"@pid":"69/2960","text":"Rayna Dimitrova"},{"@pid":"71/1981","text":"Rupak Majumdar"}]},"title":"Symbolic Model Checking for Factored Probabilistic Models.","venue":"ATVA","pages":"444-460","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/DeiningerDM16","doi":"10.1007/978-3-319-46520-3_28","ee":"https://doi.org/10.1007/978-3-319-46520-3_28","url":"https://dblp.org/rec/conf/atva/DeiningerDM16"}, "url":"URL#3210862" }, { "@score":"1", "@id":"3210863", "info":{"authors":{"author":[{"@pid":"43/6032","text":"Alexandre Duret-Lutz"},{"@pid":"07/2336","text":"Fabrice Kordon"},{"@pid":"10/683","text":"Denis Poitrenaud"},{"@pid":"41/9726","text":"Etienne Renault"}]},"title":"Heuristics for Checking Liveness Properties with Partial Order Reductions.","venue":"ATVA","pages":"340-356","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/Duret-LutzKPR16","doi":"10.1007/978-3-319-46520-3_22","ee":"https://doi.org/10.1007/978-3-319-46520-3_22","url":"https://dblp.org/rec/conf/atva/Duret-LutzKPR16"}, "url":"URL#3210863" }, { "@score":"1", "@id":"3210864", "info":{"authors":{"author":[{"@pid":"43/6032","text":"Alexandre Duret-Lutz"},{"@pid":"187/1632","text":"Alexandre Lewkowicz"},{"@pid":"187/1605","text":"Amaury Fauchille"},{"@pid":"167/2076","text":"Thibaud Michaud"},{"@pid":"41/9726","text":"Etienne Renault"},{"@pid":"187/1553","text":"Laurent Xu"}]},"title":"Spot 2.0 - A Framework for LTL and \\omega -Automata Manipulation.","venue":"ATVA","pages":"122-129","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/Duret-LutzLFMRX16","doi":"10.1007/978-3-319-46520-3_8","ee":"https://doi.org/10.1007/978-3-319-46520-3_8","url":"https://dblp.org/rec/conf/atva/Duret-LutzLFMRX16"}, "url":"URL#3210864" }, { "@score":"1", "@id":"3210865", "info":{"authors":{"author":[{"@pid":"73/4443","text":"Bernd Finkbeiner"},{"@pid":"s/HelmutSeidl","text":"Helmut Seidl"},{"@pid":"50/5380-8","text":"Christian Müller 0008"}]},"title":"Specifying and Verifying Secrecy in Workflows with Arbitrarily Many Agents.","venue":"ATVA","pages":"157-173","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/FinkbeinerS016","doi":"10.1007/978-3-319-46520-3_11","ee":"https://doi.org/10.1007/978-3-319-46520-3_11","url":"https://dblp.org/rec/conf/atva/FinkbeinerS016"}, "url":"URL#3210865" }, { "@score":"1", "@id":"3210866", "info":{"authors":{"author":[{"@pid":"73/4443","text":"Bernd Finkbeiner"},{"@pid":"140/9733","text":"Hazem Torfah"}]},"title":"Synthesizing Skeletons for Reactive Systems.","venue":"ATVA","pages":"271-286","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/FinkbeinerT16","doi":"10.1007/978-3-319-46520-3_18","ee":"https://doi.org/10.1007/978-3-319-46520-3_18","url":"https://dblp.org/rec/conf/atva/FinkbeinerT16"}, "url":"URL#3210866" }, { "@score":"1", "@id":"3210867", "info":{"authors":{"author":{"@pid":"56/1768","text":"Masahiro Fujita"}},"title":"Synthesizing and Completely Testing Hardware Based on Templates Through Small Numbers of Test Patterns.","venue":"ATVA","pages":"3-10","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/Fujita16","doi":"10.1007/978-3-319-46520-3_1","ee":"https://doi.org/10.1007/978-3-319-46520-3_1","url":"https://dblp.org/rec/conf/atva/Fujita16"}, "url":"URL#3210867" }, { "@score":"1", "@id":"3210868", "info":{"authors":{"author":[{"@pid":"187/1596","text":"Jinru Hua"},{"@pid":"k/SarfrazKhurshid","text":"Sarfraz Khurshid"}]},"title":"A Sketching-Based Approach for Debugging Using Test Cases.","venue":"ATVA","pages":"463-478","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/HuaK16","doi":"10.1007/978-3-319-46520-3_29","ee":"https://doi.org/10.1007/978-3-319-46520-3_29","url":"https://dblp.org/rec/conf/atva/HuaK16"}, "url":"URL#3210868" }, { "@score":"1", "@id":"3210869", "info":{"authors":{"author":[{"@pid":"81/5510","text":"Radu Iosif"},{"@pid":"45/2701","text":"Arnaud Sangnier"}]},"title":"How Hard is It to Verify Flat Affine Counter Systems with the Finite Monoid Property?","venue":"ATVA","pages":"89-105","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/IosifS16","doi":"10.1007/978-3-319-46520-3_6","ee":"https://doi.org/10.1007/978-3-319-46520-3_6","url":"https://dblp.org/rec/conf/atva/IosifS16"}, "url":"URL#3210869" }, { "@score":"1", "@id":"3210870", "info":{"authors":{"author":[{"@pid":"21/8279","text":"Denis Kuperberg"},{"@pid":"75/6016","text":"Julien Brunel"},{"@pid":"65/4674","text":"David Chemouil"}]},"title":"On Finite Domains in First-Order Linear Temporal Logic.","venue":"ATVA","pages":"211-226","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/KuperbergBC16","doi":"10.1007/978-3-319-46520-3_14","ee":"https://doi.org/10.1007/978-3-319-46520-3_14","url":"https://dblp.org/rec/conf/atva/KuperbergBC16"}, "url":"URL#3210870" }, { "@score":"1", "@id":"3210871", "info":{"authors":{"author":[{"@pid":"09/1365","text":"Xin Li"},{"@pid":"k/NaokiKobayashi","text":"Naoki Kobayashi 0001"}]},"title":"Equivalence-Based Abstraction Refinement for \\mu HORS Model Checking.","venue":"ATVA","pages":"304-320","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/Li016","doi":"10.1007/978-3-319-46520-3_20","ee":"https://doi.org/10.1007/978-3-319-46520-3_20","url":"https://dblp.org/rec/conf/atva/Li016"}, "url":"URL#3210871" }, { "@score":"1", "@id":"3210872", "info":{"authors":{"author":[{"@pid":"168/1149","text":"Matteo Marescotti"},{"@pid":"50/5894","text":"Antti E. J. Hyvärinen"},{"@pid":"12/2269","text":"Natasha Sharygina"}]},"title":"Clause Sharing and Partitioning for Cloud-Based SMT Solving.","venue":"ATVA","pages":"428-443","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/MarescottiHS16","doi":"10.1007/978-3-319-46520-3_27","ee":"https://doi.org/10.1007/978-3-319-46520-3_27","url":"https://dblp.org/rec/conf/atva/MarescottiHS16"}, "url":"URL#3210872" }, { "@score":"1", "@id":"3210873", "info":{"authors":{"author":[{"@pid":"127/1049","text":"Óscar Martín 0001"},{"@pid":"70/253","text":"Alberto Verdejo"},{"@pid":"34/4176","text":"Narciso Martí-Oliet"}]},"title":"Synchronous Products of Rewrite Systems.","venue":"ATVA","pages":"141-156","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/MartinVM16","doi":"10.1007/978-3-319-46520-3_10","ee":"https://doi.org/10.1007/978-3-319-46520-3_10","url":"https://dblp.org/rec/conf/atva/MartinVM16"}, "url":"URL#3210873" }, { "@score":"1", "@id":"3210874", "info":{"authors":{"author":[{"@pid":"180/8234","text":"Patrick Metzler"},{"@pid":"139/3187","text":"Habib Saissi"},{"@pid":"43/3529","text":"Péter Bokor"},{"@pid":"187/1593","text":"Robin Hesse"},{"@pid":"s/NeerajSuri","text":"Neeraj Suri"}]},"title":"Efficient Verification of Program Fragments: Eager POR.","venue":"ATVA","pages":"375-391","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/MetzlerSBHS16","doi":"10.1007/978-3-319-46520-3_24","ee":"https://doi.org/10.1007/978-3-319-46520-3_24","url":"https://dblp.org/rec/conf/atva/MetzlerSBHS16"}, "url":"URL#3210874" }, { "@score":"1", "@id":"3210875", "info":{"authors":{"author":[{"@pid":"118/3833","text":"Philipp J. Meyer"},{"@pid":"62/964","text":"Michael Luttenberger"}]},"title":"Solving Mean-Payoff Games on the GPU.","venue":"ATVA","pages":"262-267","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/MeyerL16","doi":"10.1007/978-3-319-46520-3_17","ee":"https://doi.org/10.1007/978-3-319-46520-3_17","url":"https://dblp.org/rec/conf/atva/MeyerL16"}, "url":"URL#3210875" }, { "@score":"1", "@id":"3210876", "info":{"authors":{"author":[{"@pid":"169/6342","text":"Thomas Neele"},{"@pid":"77/6678","text":"Anton Wijs"},{"@pid":"38/2132","text":"Dragan Bosnacki"},{"@pid":"p/JvdPol","text":"Jaco van de Pol"}]},"title":"Partial-Order Reduction for GPU Model Checking.","venue":"ATVA","pages":"357-374","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/NeeleWBP16","doi":"10.1007/978-3-319-46520-3_23","ee":"https://doi.org/10.1007/978-3-319-46520-3_23","url":"https://dblp.org/rec/conf/atva/NeeleWBP16"}, "url":"URL#3210876" }, { "@score":"1", "@id":"3210877", "info":{"authors":{"author":[{"@pid":"147/4379","text":"Truc L. Nguyen"},{"@pid":"27/3809-2","text":"Bernd Fischer 0002"},{"@pid":"33/5041","text":"Salvatore La Torre"},{"@pid":"11/1029","text":"Gennaro Parlato"}]},"title":"Lazy Sequentialization for the Safety Verification of Unbounded Concurrent Programs.","venue":"ATVA","pages":"174-191","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/Nguyen0TP16","doi":"10.1007/978-3-319-46520-3_12","ee":"https://doi.org/10.1007/978-3-319-46520-3_12","url":"https://dblp.org/rec/conf/atva/Nguyen0TP16"}, "url":"URL#3210877" }, { "@score":"1", "@id":"3210878", "info":{"authors":{"author":[{"@pid":"187/1563","text":"Steven de Oliveira"},{"@pid":"01/5624","text":"Saddek Bensalem"},{"@pid":"05/1744","text":"Virgile Prevosto"}]},"title":"Polynomial Invariants by Linear Algebra.","venue":"ATVA","pages":"479-494","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/OliveiraBP16","doi":"10.1007/978-3-319-46520-3_30","ee":"https://doi.org/10.1007/978-3-319-46520-3_30","url":"https://dblp.org/rec/conf/atva/OliveiraBP16"}, "url":"URL#3210878" }, { "@score":"1", "@id":"3210879", "info":{"authors":{"author":[{"@pid":"120/2795","text":"Rui Qiu"},{"@pid":"03/4368","text":"Corina S. Pasareanu"},{"@pid":"k/SarfrazKhurshid","text":"Sarfraz Khurshid"}]},"title":"Certified Symbolic Execution.","venue":"ATVA","pages":"495-511","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/QiuPK16","doi":"10.1007/978-3-319-46520-3_31","ee":"https://doi.org/10.1007/978-3-319-46520-3_31","url":"https://dblp.org/rec/conf/atva/QiuPK16"}, "url":"URL#3210879" }, { "@score":"1", "@id":"3210880", "info":{"authors":{"author":[{"@pid":"162/9630","text":"Tim Quatmann"},{"@pid":"124/8982","text":"Christian Dehnert"},{"@pid":"32/8421-1","text":"Nils Jansen 0001"},{"@pid":"115/4386","text":"Sebastian Junges"},{"@pid":"k/JoostPieterKatoen","text":"Joost-Pieter Katoen"}]},"title":"Parameter Synthesis for Markov Models: Faster Than Ever.","venue":"ATVA","pages":"50-67","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/QuatmannD0JK16","doi":"10.1007/978-3-319-46520-3_4","ee":"https://doi.org/10.1007/978-3-319-46520-3_4","url":"https://dblp.org/rec/conf/atva/QuatmannD0JK16"}, "url":"URL#3210880" }, { "@score":"1", "@id":"3210881", "info":{"authors":{"author":[{"@pid":"41/9861","text":"Andrew Reynolds 0001"},{"@pid":"81/5510","text":"Radu Iosif"},{"@pid":"27/5922","text":"Cristina Serban"},{"@pid":"79/1695-1","text":"Tim King 0001"}]},"title":"A Decision Procedure for Separation Logic in SMT.","venue":"ATVA","pages":"244-261","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/ReynoldsIS016","doi":"10.1007/978-3-319-46520-3_16","ee":"https://doi.org/10.1007/978-3-319-46520-3_16","url":"https://dblp.org/rec/conf/atva/ReynoldsIS016"}, "url":"URL#3210881" }, { "@score":"1", "@id":"3210882", "info":{"authors":{"author":[{"@pid":"180/1879","text":"Hendrik Roehm"},{"@pid":"87/1596","text":"Jens Oehlerking"},{"@pid":"27/1893-1","text":"Thomas Heinz 0001"},{"@pid":"67/1387","text":"Matthias Althoff"}]},"title":"STL Model Checking of Continuous and Hybrid Systems.","venue":"ATVA","pages":"412-427","year":"2016","type":"Conference and Workshop Papers","access":"closed","key":"conf/atva/RoehmOHA16","doi":"10.1007/978-3-319-46520-3_26","ee":"https://doi.org/10.1007/978-3-319-46520-3_26","url":"https://dblp.org/rec/conf/atva/RoehmOHA16"}, "url":"URL#3210882" } ] } } } )