학술논문

Computer aided verification. Part I.
Document Type
Proceedings Paper
Author
Source
Subject
68 Computer science
  68-06 Proceedings, conferences, collections, etc.
Language
English
Abstract
{\bf Papers in this collection include the following:} \tpar \{For the 28th Conference see [MR3536854; 3536884].\} \tpar Xiaowei\ Huang, Marta\ Kwiatkowska, Sen\ Wang\ and Min\ Wu, ``Safety verification of deep neural networks'', \nbp{3--29}. 3693667 \tpar Viktor\ Vafeiadis, ``Program verification under weak memory consistency using separation logic'', \nbp{30--46}. 3693668 \tpar Loris\ D'Antoni\ and Margus\ Veanes, ``The power of symbolic automata and transducers'', \nbp{47--67}. 3693669 \tpar Xujie\ Si, Xin\ Zhang, Radu\ Grigore\ and Mayur\ Naik, ``Maximum satisfiability in software analysis: applications and techniques'', \nbp{68--94}. 3693670 \tpar Guy\ Katz, Clark\ Barrett, David\ L.\ Dill, Kyle\ Julian\ and Mykel\ J.\ Kochenderfer, ``Reluplex: an efficient SMT solver for verifying deep neural networks'', \nbp{97--117}. 3693671 \tpar Krishnendu\ Chatterjee, Hongfei\ Fu\ and Aniket\ Murhekar, ``Automated recurrence analysis for almost-linear expected-runtime bounds'', \nbp{118--139}. 3693672 \tpar Tim\ Quatmann, Sebastian\ Junges\ and Joost-Pieter\ Katoen, ``Markov automata with multiple objectives'', \nbp{140--159}. 3693673 \tpar Christel\ Baier, Joachim\ Klein, Linda\ Leuschner, David\ Parker\ and Sascha\ Wunderlich, ``Ensuring the reliability of your model checker: interval iteration for Markov decision processes'', \nbp{160--180}. 3693674 \tpar Aws\ Albarghouthi, Loris\ D'Antoni\ and Samuel\ Drews, ``Repairing decision-making programs under uncertainty'', \nbp{181--200}. 3693675 \tpar Pranav\ Ashok, Krishnendu\ Chatterjee, Przemysław\ Daca, Jan\ Křetínský\ and Tobias\ Meggendorfer, ``Value iteration for long-run average reward in Markov decision processes'', \nbp{201--221}. 3693676 \tpar Hendrik\ Roehm, Thomas\ Heinz\ and Eva\ Charlotte\ Mayer, ``STLInspector: STL validation with guarantees'', \nbp{225--232}. 3693677 \tpar Pavol\ Bielik, Veselin\ Raychev\ and Martin\ Vechev, ``Learning a static analyzer from data'', \nbp{233--253}. 3693678 \tpar Dana\ Drachsler-Cohen, Sharon\ Shoham\ and Eran\ Yahav, ``Synthesis with abstract examples'', \nbp{254--278}. 3693679 \tpar Sarah\ Chasins\ and Phitchaya\ Mangpo\ Phothilimthana, ``Data-driven synthesis of full probabilistic programs'', \nbp{279--304}. 3693681 \tpar Marcell\ Vazquez-Chanlatte, Jyotirmoy\ V.\ Deshmukh, Xiaoqing\ Jin\ and Sanjit\ A.\ Seshia, ``Logical clustering and learning for time-series data'', \nbp{305--325}. 3693682 \tpar Dogan\ Ulus, ``MONTRE: a tool for monitoring timed regular expressions'', \nbp{329--335}. \tpar Konstantin\ Selyunin, Stefan\ Jaksic, Thang\ Nguyen, Christian\ Reidl, Udo\ Hafner, Ezio\ Bartocci, Dejan\ Nickovic\ and Radu\ Grosu, ``Runtime monitoring with recovery of the SENT communication protocol'', \nbp{336--355}. \tpar David\ Basin, Felix\ Klaedtke\ and Eugen\ Zălinescu, ``Runtime verification of temporal properties over out-of-order data streams'', \nbp{356--376}. 3693680 \tpar Jacek\ Cyranka, Md.\ Ariful\ Islam, Greg\ Byrne, Paul\ Jones, Scott\ A.\ Smolka\ and Radu\ Grosu, ``Lagrangian reachability'', \nbp{379--400}. 3693685 \tpar Stanley\ Bak\ and Parasara\ Sridhar\ Duggirala, ``Simulation-equivalent reachability of large linear systems with inputs'', \nbp{401--420}. 3693686 \tpar Thomas\ Brihaye, Gilles\ Geeraerts, Hsi-Ming\ Ho\ and Benjamin\ Monmege, ``MIGHTYL: a compositional translation from MITL to timed automata'', \nbp{421--440}. \tpar Chuchu\ Fan, Bolun\ Qi, Sayan\ Mitra\ and Mahesh\ Viswanathan, ``DRYVR: data-driven verification and compositional reasoning for automotive systems'', \nbp{441--461}. \tpar Alessandro\ Abate, Iury\ Bessa, Dario\ Cattaruzza, Lucas\ Cordeiro, Cristina\ David, Pascal\ Kesseli, Daniel\ Kroening\ and Elizabeth\ Polgreen, ``Automated formal synthesis of digital controllers for state-space physical plants'', \nbp{462--482}. \tpar Arvind\ Adimoolam, Thao\ Dang, Alexandre\ Donzé, James\ Kapinski\ and Xiaoqing\ Jin, ``Classification and coverage-based falsification for embedded control systems'', \nbp{483--503}. \tpar Rajeev\ Alur, Joseph\ Devietti, Omar\ S.\ Navarro Leija\ and Nimit\ Singhania, ``GPUDrano: detecting uncoalesced accesses in GPU programs'', \nbp{507--525}. \tpar Elvira\ Albert, Puri\ Arenas, María\ García de la Banda, Miguel\ Gómez-Zamalloa\ and Peter\ J.\ Stuckey, ``Context-sensitive dynamic partial order reduction'', \nbp{526--543}. 3693692 \tpar Matt\ Windsor, Mike\ Dodds, Ben\ Simner\ and Matthew\ J.\ Parkinson, ``Starling: lightweight concurrency verification with views'', \nbp{544--569}. 3693693 \tpar Anton\ Wijs\ and Thomas\ Neele, ``Compositional model checking with incremental counter-example construction'', \nbp{570--590}. 3693694 \tpar Nikola\ Beneš, Luboš\ Brim, Martin\ Demko, Samuel\ Pastva\ and David\ Šafránek, ``Pithya: a parallel tool for parameter synthesis of piecewise multi-affine dynamical systems'', \nbp{591--598}. \tpar

Online Access