Software Transactional Memory on Relaxed Memory Models (English)
Free access
- New search for: Guerraoui, Rachid
- New search for: Henzinger, Thomas A.
- New search for: Singh, Vasu
- New search for: Guerraoui, Rachid
- New search for: Henzinger, Thomas A.
- New search for: Singh, Vasu
In:
Computer Aided Verification
3
;
321-336
;
2009
- Article/Chapter (Book) / Electronic Resource
-
Title:Software Transactional Memory on Relaxed Memory Models
-
Contributors:
-
Published in:Computer Aided Verification , 3 ; 321-336Lecture Notes in Computer Science ; 5643, 3 ; 321-336
-
Publisher:
- New search for: Springer Berlin Heidelberg
-
Place of publication:Berlin, Heidelberg
-
Publication date:2009-01-01
-
Size:16 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
-
Transactional Memory: Glimmer of a TheoryGuerraoui, Rachid / Kapałka, Michał et al. | 2009
- 16
-
Mixed-Signal System Verification: A High-Speed Link ExampleKim, Jaeha et al. | 2009
- 17
-
Modelling Epigenetic Information Maintenance: A Kappa TutorialKrivine, Jean / Danos, Vincent / Benecke, Arndt et al. | 2009
- 33
-
Component-Based Construction of Real-Time Systems in BIPSifakis, Joseph et al. | 2009
- 35
-
Models and Proofs of Protocol Security: A Progress ReportAbadi, Martín / Blanchet, Bruno / Comon-Lundh, Hubert et al. | 2009
- 50
-
Predictability vs. Efficiency in the Multicore Era: Fight of Titans or Happy Ever after?Benini, Luca et al. | 2009
- 51
-
SPEED: Symbolic Complexity Bound AnalysisGulwani, Sumit et al. | 2009
- 63
-
Regression Verification: Proving the Equivalence of Similar ProgramsStrichman, Ofer et al. | 2009
- 64
-
Symbolic Counter Abstraction for Concurrent SoftwareBasler, Gérard / Mazzucchi, Michele / Wahl, Thomas / Kroening, Daniel et al. | 2009
- 79
-
Priority Scheduling of Distributed Systems Based on Model CheckingBasu, Ananda / Bensalem, Saddek / Peled, Doron / Sifakis, Joseph et al. | 2009
- 94
-
Explaining Counterexamples Using CausalityBeer, Ilan / Ben-David, Shoham / Chockler, Hana / Orni, Avigail / Trefler, Richard et al. | 2009
- 109
-
Size-Change Termination, Monotonicity Constraints and Ranking FunctionsBen-Amram, Amir M. et al. | 2009
- 124
-
Linear Functional Fixed-pointsBjørner, Nikolaj / Hendrix, Joe et al. | 2009
- 140
-
Better Quality in Synthesis through Quantitative ObjectivesBloem, Roderick / Chatterjee, Krishnendu / Henzinger, Thomas A. / Jobstmann, Barbara et al. | 2009
- 157
-
Automatic Verification of Integer Array ProgramsBozga, Marius / Habermehl, Peter / Iosif, Radu / Konečný, Filip / Vojnar, Tomáš et al. | 2009
- 173
-
Automated Analysis of Java Methods for ConfidentialityČerný, Pavol / Alur, Rajeev et al. | 2009
- 188
-
Requirements Validation for Hybrid SystemsCimatti, Alessandro / Roveri, Marco / Tonetta, Stefano et al. | 2009
- 204
-
Towards Performance Prediction of Compositional Models in Industrial GALS DesignsCoste, Nicolas / Hermanns, Holger / Lantreibecq, Etienne / Serwe, Wendelin et al. | 2009
- 219
-
Image Computation for Polynomial Dynamical Systems Using the Bernstein ExpansionDang, Thao / Salinas, David et al. | 2009
- 233
-
Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over IntegersDillig, Isil / Dillig, Thomas / Aiken, Alex et al. | 2009
- 248
-
Meta-analysis for Atomicity Violations under Nested LockingFarzan, Azadeh / Madhusudan, P. / Sorrentino, Francesco et al. | 2009
- 263
-
An Antichain Algorithm for LTL RealizabilityFiliot, Emmanuel / Jin, Naiyong / Raskin, Jean-François et al. | 2009
- 278
-
On Extending Bounded Proofs to Inductive ProofsFuhrmann, Oded / Hoory, Shlomo et al. | 2009
- 291
-
Games through Nested FixpointsGawlitza, Thomas Martin / Seidl, Helmut et al. | 2009
- 306
-
Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo TheoriesGe, Yeting / Moura, Leonardo et al. | 2009
- 321
-
Software Transactional Memory on Relaxed Memory ModelsGuerraoui, Rachid / Henzinger, Thomas A. / Singh, Vasu et al. | 2009
- 337
-
Sliding Window Abstraction for Infinite Markov ChainsHenzinger, Thomas A. / Mateescu, Maria / Wolf, Verena et al. | 2009
- 353
-
Centaur Technology Media Unit VerificationHunt, Warren A. Jr. / Swords, Sol et al. | 2009
- 368
-
Incremental Instance Generation in Local ReasoningJacobs, Swen et al. | 2009
- 383
-
Quantifier Elimination via Functional CompositionJiang, Jie-Hong R. et al. | 2009
- 398
-
Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction TechniqueKahlon, Vineet / Wang, Chao / Gupta, Aarti et al. | 2009
- 414
-
Replacing Testing with Formal Verification in Intel $^{\scriptsize\circledR}$ CoreTM i7 Processor Execution Engine ValidationKaivola, Roope / Ghughal, Rajnish / Narasimhan, Naren / Telfer, Amber / Whittemore, Jesse / Pandav, Sudhindra / Slobodová, Anna / Taylor, Christopher / Frolov, Vladimir / Reeber, Erik et al. | 2009
- 430
-
Generating and Analyzing Symbolic Traces of Simulink/Stateflow ModelsKanade, Aditya / Alur, Rajeev / Ivančić, Franjo / Ramesh, S. / Sankaranarayanan, Sriram / Shashidhar, K. C. et al. | 2009
- 446
-
A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer ConstraintsKitchen, Nathan / Kuehlmann, Andreas et al. | 2009
- 462
-
Generalizing DPLL to Richer LogicsMcMillan, Kenneth L. / Kuehlmann, Andreas / Sagiv, Mooly et al. | 2009
- 477
-
Reducing Context-Bounded Concurrent Reachability to Sequential ReachabilityTorre, Salvatore / Madhusudan, P. / Parlato, Gennaro et al. | 2009
- 493
-
Intra-module InferenceLahiri, Shuvendu K. / Qadeer, Shaz / Galeotti, Juan P. / Voung, Jan W. / Wies, Thomas et al. | 2009
- 509
-
Static and Precise Detection of Concurrency Errors in Systems Code Using SMT SolversLahiri, Shuvendu K. / Qadeer, Shaz / Rakamarić, Zvonimir et al. | 2009
- 525
-
Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular ConstraintsLammich, Peter / Müller-Olm, Markus / Wenner, Alexander et al. | 2009
- 540
-
Reachability Analysis of Hybrid Systems Using Support FunctionsGuernic, Colas / Girard, Antoine et al. | 2009
- 555
-
Reducing Test Inputs Using Information PartitionsMajumdar, Rupak / Xu, Ru-Gang et al. | 2009
- 570
-
On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision ProcedureMonniaux, David et al. | 2009
- 584
-
Cardinality Abstraction for Declarative Networking ApplicationsPérez, Juan Antonio Navarro / Rybalchenko, Andrey / Singh, Atul et al. | 2009
- 599
-
Equivalence Checking of Static Affine Programs Using Widening to Handle RecurrencesVerdoolaege, Sven / Janssens, Gerda / Bruynooghe, Maurice et al. | 2009
- 614
-
D-Finder: A Tool for Compositional Deadlock Detection and VerificationBensalem, Saddek / Bozga, Marius / Nguyen, Thanh-Hung / Sifakis, Joseph et al. | 2009
- 620
-
HybridFluctuat: A Static Analyzer of Numerical Programs within a Continuous EnvironmentBouissou, Olivier / Goubault, Eric / Putot, Sylvie / Tekkal, Karim / Vedrine, Franck et al. | 2009
- 627
-
The Zonotope Abstract Domain Taylor1+Ghorbal, Khalil / Goubault, Eric / Putot, Sylvie et al. | 2009
- 634
-
InvGen: An Efficient Invariant GeneratorGupta, Ashutosh / Rybalchenko, Andrey et al. | 2009
- 641
-
INFAMY: An Infinite-State Markov Model CheckerHahn, Ernst Moritz / Hermanns, Holger / Wachter, Björn / Zhang, Lijun et al. | 2009
- 648
-
Browser-Based Enforcement of Interface Contracts in Web Applications with BeepBeepHallé, Sylvain / Villemaire, Roger et al. | 2009
- 654
-
Homer: A Higher-Order Observational Equivalence Model checkERHopkins, David / Ong, C. -H. Luke et al. | 2009
- 661
-
Apron: A Library of Numerical Abstract Domains for Static AnalysisJeannet, Bertrand / Miné, Antoine et al. | 2009
- 668
-
Beaver: Engineering an Efficient SMT Solver for Bit-Vector ArithmeticJha, Susmit / Limaye, Rhishikesh / Seshia, Sanjit A. et al. | 2009
- 675
-
CalFuzzer: An Extensible Active Testing Framework for Concurrent ProgramsJoshi, Pallavi / Naik, Mayur / Park, Chang-Seo / Sen, Koushik et al. | 2009
- 682
-
MCMAS: A Model Checker for the Verification of Multi-Agent SystemsLomuscio, Alessio / Qu, Hongyang / Raimondi, Franco et al. | 2009
- 689
-
TASS: Timing Analyzer of Scenario-Based SpecificationsPan, Minxue / Bu, Lei / Li, Xuandong et al. | 2009
- 696
-
Translation Validation: From Simulink to CRyabtsev, Michael / Strichman, Ofer et al. | 2009
- 702
-
VS3: SMT Solvers for Program VerificationSrivastava, Saurabh / Gulwani, Sumit / Foster, Jeffrey S. et al. | 2009
- 709
-
PAT: Towards Flexible Verification under FairnessSun, Jun / Liu, Yang / Dong, Jin Song / Pang, Jun et al. | 2009
- 715
-
A Concurrent Portfolio Approach to SMT SolvingWintersteiger, Christoph M. / Hamadi, Youssef / Moura, Leonardo et al. | 2009