Software Model Checking for People Who Love Automata (English)
Free access
- New search for: Heizmann, Matthias
- New search for: Hoenicke, Jochen
- New search for: Podelski, Andreas
- New search for: Heizmann, Matthias
- New search for: Hoenicke, Jochen
- New search for: Podelski, Andreas
In:
Computer Aided Verification
1
;
36-52
;
2013
- Article/Chapter (Book) / Electronic Resource
-
Title:Software Model Checking for People Who Love Automata
-
Contributors:
-
Published in:Computer Aided Verification , 1 ; 36-52Lecture Notes in Computer Science ; 8044, 1 ; 36-52
-
Publisher:
- New search for: Springer Berlin Heidelberg
-
Place of publication:Berlin, Heidelberg
-
Publication date:2013-01-01
-
Size:17 pages
-
ISBN:
-
ISSN:
-
DOI:
-
Type of media:Article/Chapter (Book)
-
Type of material:Electronic Resource
-
Language:English
-
Keywords:
-
Source:
Table of contents eBook
The tables of contents are generated automatically and are based on the data records of the individual contributions available in the index of the TIB portal. The display of the Tables of Contents may therefore be incomplete.
- 1
-
First-Order Theorem Proving and VampireKovács, Laura / Voronkov, Andrei et al. | 2013
- 36
-
Software Model Checking for People Who Love AutomataHeizmann, Matthias / Hoenicke, Jochen / Podelski, Andreas et al. | 2013
- 53
-
Multi-solver Support in Symbolic ExecutionPalikareva, Hristina / Cadar, Cristian et al. | 2013
- 69
-
Under-Approximating Cut Sets for Reachability in Large Scale Automata NetworksPaulevé, Loïc / Andrieux, Geoffroy / Koeppl, Heinz et al. | 2013
- 85
-
Model-Checking Signal Transduction Networks through Decreasing Reachability SetsClaessen, Koen / Fisher, Jasmin / Ishtiaq, Samin / Piterman, Nir / Wang, Qinsi et al. | 2013
- 101
-
TTP: Tool for Tumor ProgressionReiter, Johannes G. / Bozic, Ivana / Chatterjee, Krishnendu / Nowak, Martin A. et al. | 2013
- 107
-
Exploring Parameter Space of Stochastic Biochemical Systems Using Quantitative Model CheckingBrim, Luboš / Češka, Milan / Dražan, Sven / Šafránek, David et al. | 2013
- 124
-
Parameterized Verification of Asynchronous Shared-Memory SystemsEsparza, Javier / Ganty, Pierre / Majumdar, Rupak et al. | 2013
- 141
-
Partial Orders for Efficient Bounded Model Checking of Concurrent SoftwareAlglave, Jade / Kroening, Daniel / Tautschnig, Michael et al. | 2013
- 158
-
Incremental, Inductive CoverabilityKloos, Johannes / Majumdar, Rupak / Niksic, Filip / Piskac, Ruzica et al. | 2013
- 174
-
Automatic Linearizability Proofs of Concurrent Objects with Cooperating UpdatesDrăgoi, Cezara / Gupta, Ashutosh / Henzinger, Thomas A. et al. | 2013
- 191
-
Duet: Static Analysis for Unbounded ParallelismFarzan, Azadeh / Kincaid, Zachary et al. | 2013
- 197
-
SVA and PSL Local Variables - A Practical ApproachArmoni, Roy / Fisman, Dana / Jin, Naiyong et al. | 2013
- 213
-
Formal Verification of Hardware SynthesisBraibant, Thomas / Chlipala, Adam et al. | 2013
- 229
-
CacBDD: A BDD Package with Dynamic Cache ManagementLv, Guanfeng / Su, Kaile / Xu, Yanyan et al. | 2013
- 235
-
Distributed Explicit State Model Checking of Deadlock FreedomBingham, Brad / Bingham, Jesse / Erickson, John / Greenstreet, Mark et al. | 2013
- 242
-
Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid SystemsKong, Hui / He, Fei / Song, Xiaoyu / Hung, William N. N. / Gu, Ming et al. | 2013
- 258
-
Flow*: An Analyzer for Non-linear Hybrid SystemsChen, Xin / Ábrahám, Erika / Sankaranarayanan, Sriram et al. | 2013
- 264
-
Efficient Robust Monitoring for STLDonzé, Alexandre / Ferrère, Thomas / Maler, Oded et al. | 2013
- 280
-
Abstraction Based Model-Checking of Stability of Hybrid SystemsPrabhakar, Pavithra / Garcia Soto, Miriam et al. | 2013
- 296
-
System Level Formal Verification via Model Checking Driven SimulationMancini, Toni / Mari, Federico / Massini, Annalisa / Melatti, Igor / Merli, Fabio / Tronci, Enrico et al. | 2013
- 313
-
Beautiful InterpolantsAlbarghouthi, Aws / McMillan, Kenneth L. et al. | 2013
- 330
-
Efficient Generation of Small Interpolants in CNFVizel, Yakir / Ryvchin, Vadim / Nadel, Alexander et al. | 2013
- 347
-
Disjunctive Interpolants for Horn-Clause VerificationRümmer, Philipp / Hojjat, Hossein / Kuncak, Viktor et al. | 2013
- 364
-
Generating Non-linear Interpolants by Semidefinite ProgrammingDai, Liyun / Xia, Bican / Zhan, Naijun et al. | 2013
- 381
-
Under-Approximating Loops in C Programs for Fast Counterexample DetectionKroening, Daniel / Lewis, Matt / Weissenbacher, Georg et al. | 2013
- 397
-
Proving Termination Starting from the EndGanty, Pierre / Genaim, Samir et al. | 2013
- 413
-
Better Termination Proving through CooperationBrockschmidt, Marc / Cook, Byron / Fuhs, Carsten et al. | 2013
- 430
-
Relative Equivalence in the Presence of AmbiguityAdler, Oshri / Eisner, Cindy / Veksler, Tatyana et al. | 2013
- 447
-
Combining Relational Learning with SMT Solvers Using CEGARChaganty, Arun / Lal, Akash / Nori, Aditya V. / Rajamani, Sriram K. et al. | 2013
- 463
-
A Fully Verified Executable LTL Model CheckerEsparza, Javier / Lammich, Peter / Neumann, René / Nipkow, Tobias / Schimpf, Alexander / Smaus, Jan-Georg et al. | 2013
- 479
-
Automatic Generation of Quality SpecificationsAlmagor, Shaull / Avni, Guy / Kupferman, Orna et al. | 2013
- 495
-
Upper Bounds for Newton’s Method on Monotone Polynomial Systems, and P-Time Model Checking of Probabilistic One-Counter AutomataStewart, Alistair / Etessami, Kousha / Yannakakis, Mihalis et al. | 2013
- 511
-
Probabilistic Program Analysis with MartingalesChakarov, Aleksandar / Sankaranarayanan, Sriram et al. | 2013
- 527
-
Polynomial-Time Verification of PCTL Properties of MDPs with Convex UncertaintiesPuggelli, Alberto / Li, Wenchao / Sangiovanni-Vincentelli, Alberto L. / Seshia, Sanjit A. et al. | 2013
- 543
-
Faster Algorithms for Markov Decision Processes with Low TreewidthChatterjee, Krishnendu / Łącki, Jakub et al. | 2013
- 559
-
Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL SynthesisChatterjee, Krishnendu / Gaiser, Andreas / Křetínský, Jan et al. | 2013
- 576
-
Importance Splitting for Statistical Model Checking Rare PropertiesJegourel, Cyrille / Legay, Axel / Sedwards, Sean et al. | 2013
- 592
-
Minimal Sets over Monotone Predicates in Boolean FormulaeMarques-Silva, Joao / Janota, Mikoláš / Belov, Anton et al. | 2013
- 608
-
A Scalable and Nearly Uniform Generator of SAT WitnessesChakraborty, Supratik / Meel, Kuldeep S. / Vardi, Moshe Y. et al. | 2013
- 624
-
Equivalence of Extended Symbolic Finite TransducersD’Antoni, Loris / Veanes, Margus et al. | 2013
- 640
-
Finite Model Finding in SMTReynolds, Andrew / Tinelli, Cesare / Goel, Amit / Krstić, Sava et al. | 2013
- 656
-
JBernstein: A Validity Checker for Generalized Polynomial ConstraintsCheng, Chih-Hong / Ruess, Harald / Shankar, Natarajan et al. | 2013
- 662
-
ILP Modulo TheoriesManolios, Panagiotis / Papavasileiou, Vasilis et al. | 2013
- 678
-
Smten: Automatic Translation of High-Level Symbolic Computations into SMT QueriesUhler, Richard / Dave, Nirav et al. | 2013
- 684
-
Explain: A Tool for Performing Abductive InferenceDillig, Isil / Dillig, Thomas et al. | 2013
- 690
-
A Tool for Estimating Information LeakageChothia, Tom / Kawamoto, Yusuke / Novakovic, Chris et al. | 2013
- 696
-
The TAMARIN Prover for the Symbolic Analysis of Security ProtocolsMeier, Simon / Schmidt, Benedikt / Cremers, Cas / Basin, David et al. | 2013
- 702
-
QUAIL: A Quantitative Security Analyzer for Imperative CodeBiondi, Fabrizio / Legay, Axel / Traonouez, Louis-Marie / Wąsowski, Andrzej et al. | 2013
- 708
-
Lengths May Break Privacy – Or How to Check for Equivalences with LengthCheval, Vincent / Cortier, Véronique / Plet, Antoine et al. | 2013
- 724
-
Finding Security Vulnerabilities in a Network Protocol Using Parameterized SystemsSosnovich, Adi / Grumberg, Orna / Nakibly, Gabi et al. | 2013
- 740
-
Fully Automated Shape Analysis Based on Forest AutomataHolík, Lukáš / Lengál, Ondřej / Rogalewicz, Adam / Šimáček, Jiří / Vojnar, Tomáš et al. | 2013
- 756
-
Effectively-Propositional Reasoning about Reachability in Linked Data StructuresItzhaky, Shachar / Banerjee, Anindya / Immerman, Neil / Nanevski, Aleksandar / Sagiv, Mooly et al. | 2013
- 773
-
Automating Separation Logic Using SMTPiskac, Ruzica / Wies, Thomas / Zufferey, Damien et al. | 2013
- 790
-
SeLoger: A Tool for Graph-Based Reasoning in Separation LogicHaase, Christoph / Ishtiaq, Samin / Ouaknine, Joël / Parkinson, Matthew J. et al. | 2013
- 796
-
Validating Library Usage InteractivelyHarris, William R. / Jin, Guoliang / Lu, Shan / Jha, Somesh et al. | 2013
- 813
-
Learning Universally Quantified Invariants of Linear Data StructuresGarg, Pranav / Löding, Christof / Madhusudan, P. / Neider, Daniel et al. | 2013
- 830
-
Towards Distributed Software Model-Checking Using Decision DiagramsColange, Maximilien / Baarir, Souheib / Kordon, Fabrice / Thierry-Mieg, Yann et al. | 2013
- 846
-
Automatic Abstraction in SMT-Based Unbounded Software Model CheckingKomuravelli, Anvesh / Gurfinkel, Arie / Chaki, Sagar / Clarke, Edmund M. et al. | 2013
- 863
-
DiVinE 3.0 – An Explicit-State Model Checker for Multithreaded C & C++ ProgramsBarnat, Jiří / Brim, Luboš / Havel, Vojtěch / Havlíček, Jan / Kriho, Jan / Lenčo, Milan / Ročkai, Petr / Štill, Vladimír / Weiser, Jiří et al. | 2013
- 869
-
Solving Existentially Quantified Horn ClausesBeyene, Tewodros A. / Popeea, Corneliu / Rybalchenko, Andrey et al. | 2013
- 883
-
GOAL for Games, Omega-Automata, and LogicsTsai, Ming-Hsien / Tsay, Yih-Kuen / Hwang, Yu-Shiang et al. | 2013
- 890
-
PRALINE: A Tool for Computing Nash Equilibria in Concurrent GamesBrenguier, Romain et al. | 2013
- 896
-
Program Repair without RegretEssen, Christian / Jobstmann, Barbara et al. | 2013
- 912
-
Programs from Proofs – A PCC AlternativeWonisch, Daniel / Schremmer, Alexander / Wehrheim, Heike et al. | 2013
- 928
-
PARTY Parameterized Synthesis of Token RingsKhalimov, Ayrat / Jacobs, Swen / Bloem, Roderick et al. | 2013
- 934
-
Recursive Program SynthesisAlbarghouthi, Aws / Gulwani, Sumit / Kincaid, Zachary et al. | 2013
- 951
-
Efficient Synthesis for Concurrency by Semantics-Preserving TransformationsČerný, Pavol / Henzinger, Thomas A. / Radhakrishna, Arjun / Ryzhyk, Leonid / Tarrach, Thorsten et al. | 2013
- 968
-
Multi-core Emptiness Checking of Timed Büchi Automata Using Inclusion AbstractionLaarman, Alfons / Olesen, Mads Chr. / Dalsgaard, Andreas Engelbredt / Larsen, Kim Guldstrand / Pol, Jaco et al. | 2013
- 984
-
PSyHCoS: Parameter Synthesis for Hierarchical Concurrent Real-Time SystemsAndré, Étienne / Liu, Yang / Sun, Jun / Dong, Jin Song / Lin, Shang-Wei et al. | 2013
- 990
-
Lazy Abstractions for Timed AutomataHerbreteau, Frédéric / Srivathsan, B. / Walukiewicz, Igor et al. | 2013
- 1006
-
Shrinktech: A Tool for the Robustness Analysis of Timed AutomataSankur, Ocan et al. | 2013