The nuXmv Symbolic Model Checker (Englisch)
Freier Zugriff
- Neue Suche nach: Cavada, Roberto
- Neue Suche nach: Cimatti, Alessandro
- Neue Suche nach: Dorigatti, Michele
- Neue Suche nach: Griggio, Alberto
- Neue Suche nach: Mariotti, Alessandro
- Neue Suche nach: Micheli, Andrea
- Neue Suche nach: Mover, Sergio
- Neue Suche nach: Roveri, Marco
- Neue Suche nach: Tonetta, Stefano
- Neue Suche nach: Cavada, Roberto
- Neue Suche nach: Cimatti, Alessandro
- Neue Suche nach: Dorigatti, Michele
- Neue Suche nach: Griggio, Alberto
- Neue Suche nach: Mariotti, Alessandro
- Neue Suche nach: Micheli, Andrea
- Neue Suche nach: Mover, Sergio
- Neue Suche nach: Roveri, Marco
- Neue Suche nach: Tonetta, Stefano
In:
Computer Aided Verification
4
;
334-342
;
2014
- Aufsatz/Kapitel (Buch) / Elektronische Ressource
-
Titel:The nuXmv Symbolic Model Checker
-
Beteiligte:Cavada, Roberto ( Autor:in ) / Cimatti, Alessandro ( Autor:in ) / Dorigatti, Michele ( Autor:in ) / Griggio, Alberto ( Autor:in ) / Mariotti, Alessandro ( Autor:in ) / Micheli, Andrea ( Autor:in ) / Mover, Sergio ( Autor:in ) / Roveri, Marco ( Autor:in ) / Tonetta, Stefano ( Autor:in )
-
Erschienen in:Computer Aided Verification , 4 ; 334-342Lecture Notes in Computer Science ; 8559, 4 ; 334-342
-
Verlag:
- Neue Suche nach: Springer International Publishing
-
Erscheinungsort:Cham
-
Erscheinungsdatum:01.01.2014
-
Format / Umfang:9 pages
-
ISBN:
-
ISSN:
-
DOI:
-
Medientyp:Aufsatz/Kapitel (Buch)
-
Format:Elektronische Ressource
-
Sprache:Englisch
-
Schlagwörter:
-
Datenquelle:
Inhaltsverzeichnis E-Book
Die Inhaltsverzeichnisse werden automatisch erzeugt und basieren auf den im Index des TIB-Portals verfügbaren Einzelnachweisen der enthaltenen Beiträge. Die Anzeige der Inhaltsverzeichnisse kann daher unvollständig oder lückenhaft sein.
- 1
-
The Spirit of Ghost CodeFilliâtre, Jean-Christophe / Gondelman, Léon / Paskevich, Andrei et al. | 2014
- 17
-
SMT-Based Model Checking for Recursive ProgramsKomuravelli, Anvesh / Gurfinkel, Arie / Chaki, Sagar et al. | 2014
- 35
-
Property-Directed Shape AnalysisItzhaky, Shachar / Bjørner, Nikolaj / Reps, Thomas / Sagiv, Mooly / Thakur, Aditya et al. | 2014
- 52
-
Shape Analysis via Second-Order Bi-AbductionLe, Quang Loc / Gherghina, Cristian / Qin, Shengchao / Chin, Wei-Ngan et al. | 2014
- 69
-
ICE: A Robust Framework for Learning InvariantsGarg, Pranav / Löding, Christof / Madhusudan, P. / Neider, Daniel et al. | 2014
- 88
-
From Invariant Checking to Invariant Inference Using Randomized SearchSharma, Rahul / Aiken, Alex et al. | 2014
- 106
-
SMACK: Decoupling Source Language Details from Verifier ImplementationsRakamarić, Zvonimir / Emmi, Michael et al. | 2014
- 114
-
Synthesis of Masking Countermeasures against Side Channel AttacksEldib, Hassan / Wang, Chao et al. | 2014
- 131
-
Temporal Mode-Checking for Runtime Monitoring of Privacy PoliciesChowdhury, Omar / Jia, Limin / Garg, Deepak / Datta, Anupam et al. | 2014
- 150
-
String Constraints for VerificationAbdulla, Parosh Aziz / Atig, Mohamed Faouzi / Chen, Yu-Fang / Holík, Lukáš / Rezine, Ahmed / Rümmer, Philipp / Stenman, Jari et al. | 2014
- 167
-
A Conference Management System with Verified Document ConfidentialityKanav, Sudeep / Lammich, Peter / Popescu, Andrei et al. | 2014
- 184
-
Vac - Verifier of Administrative Role-Based Access Control PoliciesFerrara, Anna Lisa / Madhusudan, P. / Nguyen, Truc L. / Parlato, Gennaro et al. | 2014
- 192
-
From LTL to Deterministic Automata: A Safraless Compositional ApproachEsparza, Javier / Křetínský, Jan et al. | 2014
- 209
-
Symbolic Visibly Pushdown AutomataD’Antoni, Loris / Alur, Rajeev et al. | 2014
- 226
-
Engineering a Static Verification Tool for GPU KernelsBardsley, Ethel / Betts, Adam / Chong, Nathan / Collingbourne, Peter / Deligiannis, Pantazis / Donaldson, Alastair F. / Ketema, Jeroen / Liew, Daniel / Qadeer, Shaz et al. | 2014
- 243
-
Lazy Annotation RevisitedMcMillan, Kenneth L. et al. | 2014
- 260
-
Interpolating Property Directed ReachabilityVizel, Yakir / Gurfinkel, Arie et al. | 2014
- 277
-
Verifying Relative Error Bounds Using Symbolic SimulationBingham, Jesse / Leslie-Hurd, Joe et al. | 2014
- 293
-
Regression Test Selection for Distributed Software HistoriesGligoric, Milos / Majumdar, Rupak / Sharma, Rohan / Eloussi, Lamyaa / Marinov, Darko et al. | 2014
- 310
-
GPU-Based Graph Decomposition into Strongly Connected and Maximal End ComponentsWijs, Anton / Katoen, Joost-Pieter / Bošnački, Dragan et al. | 2014
- 327
-
Software Verification in the Google App-Engine CloudBeyer, Dirk / Dresler, Georg / Wendler, Philipp et al. | 2014
- 334
-
The nuXmv Symbolic Model CheckerCavada, Roberto / Cimatti, Alessandro / Dorigatti, Michele / Griggio, Alberto / Mariotti, Alessandro / Micheli, Andrea / Mover, Sergio / Roveri, Marco / Tonetta, Stefano et al. | 2014
- 343
-
Analyzing and Synthesizing Genomic Logic FunctionsPaoletti, Nicola / Yordanov, Boyan / Hamadi, Youssef / Wintersteiger, Christoph M. / Kugler, Hillel et al. | 2014
- 358
-
Finding Instability in Biological ModelsCook, Byron / Fisher, Jasmin / Hall, Benjamin A. / Ishtiaq, Samin / Juniwal, Garvit / Piterman, Nir et al. | 2014
- 373
-
Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac CellsHuang, Zhenqi / Fan, Chuchu / Mereacre, Alexandru / Mitra, Sayan / Kwiatkowska, Marta et al. | 2014
- 391
-
Diamonds Are a Girl’s Best Friend: Partial Order Reduction for Timed Automata with AbstractionsHansen, Henri / Lin, Shang-Wei / Liu, Yang / Nguyen, Truong Khanh / Sun, Jun et al. | 2014
- 407
-
Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal ProjectionsHagemann, Willem et al. | 2014
- 424
-
Verifying LTL Properties of Hybrid Systems with K-LivenessCimatti, Alessandro / Griggio, Alberto / Mover, Sergio / Tonetta, Stefano et al. | 2014
- 441
-
Safraless Synthesis for Epistemic Temporal SpecificationsBozianu, Rodica / Dima, Cătălin / Filiot, Emmanuel et al. | 2014
- 457
-
Minimizing Running Costs in Consumption SystemsBrázdil, Tomáš / Klaška, David / Kučera, Antonín / Novotný, Petr et al. | 2014
- 473
-
CEGAR for Qualitative Analysis of Probabilistic SystemsChatterjee, Krishnendu / Chmelík, Martin / Daca, Przemysław et al. | 2014
- 491
-
Optimal Guard Synthesis for Memory SafetyDillig, Thomas / Dillig, Isil / Chaudhuri, Swarat et al. | 2014
- 508
-
Don’t Sit on the FenceAlglave, Jade / Kroening, Daniel / Nimal, Vincent / Poetzl, Daniel et al. | 2014
- 525
-
MCMAS-SLK: A Model Checker for the Verification of Strategy Logic SpecificationsČermák, Petr / Lomuscio, Alessio / Mogavero, Fabio / Murano, Aniello et al. | 2014
- 533
-
Solving Games without Controllable PredecessorNarodytska, Nina / Legg, Alexander / Bacchus, Fahiem / Ryzhyk, Leonid / Walker, Adam et al. | 2014
- 541
-
G4LTL-ST: Automatic Generation of PLC ProgramsCheng, Chih-Hong / Huang, Chung-Hao / Ruess, Harald / Stattelmann, Stefan et al. | 2014
- 550
-
Automatic Atomicity Verification for Clients of Concurrent Data StructuresLesani, Mohsen / Millstein, Todd / Palsberg, Jens et al. | 2014
- 568
-
Regression-Free Synthesis for ConcurrencyČerný, Pavol / Henzinger, Thomas A. / Radhakrishna, Arjun / Ryzhyk, Leonid / Tarrach, Thorsten et al. | 2014
- 585
-
Bounded Model Checking of Multi-threaded C Programs via Lazy SequentializationInverso, Omar / Tomasco, Ermenegildo / Fischer, Bernd / La Torre, Salvatore / Parlato, Gennaro et al. | 2014
- 603
-
An SMT-Based Approach to Coverability AnalysisEsparza, Javier / Ledesma-Garza, Ruslán / Majumdar, Rupak / Meyer, Philipp / Niksic, Filip et al. | 2014
- 620
-
LEAP: A Tool for the Parametrized Verification of Concurrent DatatypesSánchez, Alejandro / Sánchez, César et al. | 2014
- 628
-
Monadic DecompositionVeanes, Margus / Bjørner, Nikolaj / Nachmanson, Lev / Bereg, Sergey et al. | 2014
- 646
-
A DPLL(T) Theory Solver for a Theory of Strings and Regular ExpressionsLiang, Tianyi / Reynolds, Andrew / Tinelli, Cesare / Barrett, Clark / Deters, Morgan et al. | 2014
- 663
-
Bit-Vector Rewriting with Automatic Rule GenerationNadel, Alexander et al. | 2014
- 680
-
A Tale of Two Solvers: Eager and Lazy Approaches to Bit-VectorsHadarean, Liana / Bansal, Kshitij / Jovanović, Dejan / Barrett, Clark / Tinelli, Cesare et al. | 2014
- 696
-
AVATAR: The Architecture for First-Order Theorem ProversVoronkov, Andrei et al. | 2014
- 711
-
Automating Separation Logic with Trees and DataPiskac, Ruzica / Wies, Thomas / Zufferey, Damien et al. | 2014
- 729
-
A Nonlinear Real Arithmetic FragmentTiwari, Ashish / Lincoln, Patrick et al. | 2014
- 737
-
Yices 2.2Dutertre, Bruno et al. | 2014
- 745
-
A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity AnalysisSinn, Moritz / Zuleger, Florian / Veith, Helmut et al. | 2014
- 762
-
Symbolic Resource Bound Inference for Functional ProgramsMadhavan, Ravichandhran / Kuncak, Viktor et al. | 2014
- 779
-
Proving Non-termination Using Max-SMTLarraz, Daniel / Nimkar, Kaustubh / Oliveras, Albert / Rodríguez-Carbonell, Enric / Rubio, Albert et al. | 2014
- 797
-
Termination Analysis by Learning Terminating ProgramsHeizmann, Matthias / Hoenicke, Jochen / Podelski, Andreas et al. | 2014
- 814
-
Causal Termination of Multi-threaded ProgramsKupriyanov, Andrey / Finkbeiner, Bernd et al. | 2014
- 831
-
Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR)Birgmeier, Johannes / Bradley, Aaron R. / Weissenbacher, Georg et al. | 2014
- 849
-
Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath AbstractionLee, Suho / Sakallah, Karem A. et al. | 2014
- 866
-
QUICr: A Reusable Library for Parametric Abstraction of Sets and NumbersCox, Arlen / Chang, Bor-Yuh Evan / Sankaranarayanan, Sriram et al. | 2014