Skip header Section
Skip Bibliometrics Section
Spin model checker, the: primer and reference manualSeptember 2003
- Author:
- Gerard Holzmann
Skip Abstract Section
Abstract
Master SPIN, the breakthrough tool for improving software reliabilitySPIN is the world's most popular, and arguably one of the world's most powerful, tools for detecting software defects in concurrent system designs. Literally thousands of people have used SPIN since it was first introduced almost fifteen years ago. The tool has been applied to everything from the verification of complex call processing software that is used in telephone exchanges, to the validation of intricate control software for interplanetary spacecraft.This is the most comprehensive reference guide to SPIN, written by the principal designer of the tool. It covers the tool's specification language and theoretical foundation, and gives detailed advice on methods for tackling the most complex software verification problems. Sum Design and verify both abstract and detailed verification models of complex systems software Sum Develop a solid understanding of the theory behind logic model checking Sum Become an expert user of the SPIN command line interface, the Xspin graphical user interface, and the TimeLine editing tool Sum Learn the basic theory of omega automata, linear temporal logic, depth-first and breadth-first search, search optimization, and model extraction from source codeThe SPIN software was awarded the prestigious Software System Award by the Association for Computing Machinery (ACM), which previously recognized systems such as UNIX, SmallTalk, TCP/IP, Tcl/Tk, and the World Wide Web.
Cited By
Carvalho L, Degiovanni R, Cordy M, Aguirre N, Le Traon Y and Papadakis M SpecBCFuzz: Fuzzing LTL Solvers with Boundary Conditions Proceedings of the IEEE/ACM 46th International Conference on Software Engineering, (1-13)- Din C, Hähnle R, Henrio L, Johnsen E, Pun V and Tarifa S (2024). Locally Abstract, Globally Concrete Semantics of Concurrent Programming Languages, ACM Transactions on Programming Languages and Systems, 46:1, (1-58), Online publication date: 31-Mar-2024.
- André É, Liu S, Liu Y, Choppy C, Sun J and Dong J (2023). Formalizing UML State Machines for Automated Verification – A Survey, ACM Computing Surveys, 55:13s, (1-47), Online publication date: 31-Dec-2024.
- Cordy M, Lazreg S, Legay A and Schobbens P Towards Strengthening Formal Specifications with Mutation Model Checking Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, (2102-2106)
- Do C, Phyo Y, Riesco A and Ogata K (2023). Optimization Techniques for Model Checking Leads-to Properties in a Stratified Way, ACM Transactions on Software Engineering and Methodology, 32:6, (1-38), Online publication date: 30-Nov-2023.
- Päßler J, ter Beek M, Damiani F, Tapia Tarifa S and Johnsen E Formal Modelling and Analysis of a Self-Adaptive Robotic System iFM 2023, (343-363)
- Ibarra O and McQuillan I On the Containment Problem for Deterministic Multicounter Machine Models Automated Technology for Verification and Analysis, (74-94)
- Chiari M, Mandrioli D, Pontiggia F and Pradella M (2023). A Model Checker for Operator Precedence Languages, ACM Transactions on Programming Languages and Systems, 45:3, (1-66), Online publication date: 30-Sep-2023.
- Nenchev V (2023). Model checking embedded adaptive cruise controllers, Robotics and Autonomous Systems, 167:C, Online publication date: 1-Sep-2023.
- Rodríguez R, Marrone S, Marcos I and Porzio G (2023). MOSTO, Computers and Security, 132:C, Online publication date: 1-Sep-2023.
- Dimovski A, Lazreg S, Cordy M and Legay A Family-based model checking of fMultiLTL properties Proceedings of the 27th ACM International Systems and Software Product Line Conference - Volume A, (41-51)
- Serru T, Nguyen N, Batteux M and Rauzy A (2023). Minimal Critical Sequences in Model-based Safety and Security Analyses: Commonalities and Differences, ACM Transactions on Cyber-Physical Systems, 7:3, (1-20), Online publication date: 31-Jul-2023.
- Castañeda A, Hurault A, Quéinnec P and Roy M (2023). Tasks in modular proofs of concurrent algorithms, Information and Computation, 292:C, Online publication date: 1-Jun-2023.
- Ma'ayan D, Maoz S and Ringert J Anti-Patterns (Smells) in Temporal Specifications Proceedings of the 45th International Conference on Software Engineering: New Ideas and Emerging Results, (13-18)
- Panizo L and Gallardo M (2022). : analysis of data traces using an event-driven interval temporal logic, Automated Software Engineering, 30:1, Online publication date: 1-May-2023.
- Tei K, Tahara Y and Ohsuga A (2023). Towards Scalable Model Checking of Reflective Systems via Labeled Transition Systems, IEEE Transactions on Software Engineering, 49:3, (1299-1322), Online publication date: 1-Mar-2023.
- Di Giusto C, Ferré D, Laversa L and Lozes E (2023). A Partial Order View of Message-Passing Communication Models, Proceedings of the ACM on Programming Languages, 7:POPL, (1601-1627), Online publication date: 9-Jan-2023.
- Banks C, Slovak K, Coogan S and Egerstedt M Specification-Based Maneuvering of Quadcopters Through Hoops 2019 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), (5191-5197)
- Garanina N and Gorlatch S (2022). Autotuning Parallel Programs by Model Checking, Automatic Control and Computer Sciences, 56:7, (634-648), Online publication date: 1-Dec-2022.
- Zhang X, Xiao S, Li J, Pu G and Strichman O Combining BMC and Complementary Approximate Reachability to Accelerate Bug-Finding Proceedings of the 41st IEEE/ACM International Conference on Computer-Aided Design, (1-9)
- Xu B, Moss E and Blackburn S Towards a Model Checking Framework for a New Collector Framework Proceedings of the 19th International Conference on Managed Programming Languages and Runtimes, (128-139)
- Noble J, Streader D, Gariano I and Samarakoon M More Programming Than Programming: Teaching Formal Methods in a Software Engineering Programme NASA Formal Methods, (431-450)
- Kaleeswaran A, Nordmann A, Vogel T and Grunske L (2022). A systematic literature review on counterexample explanation, Information and Software Technology, 145:C, Online publication date: 1-May-2022.
- Dimovski A Model sketching by abstraction refinement for lifted model checking Proceedings of the 37th ACM/SIGAPP Symposium on Applied Computing, (1845-1848)
- Malkis A (2022). Reachability in parallel programs is polynomial in the number of threads, Journal of Parallel and Distributed Computing, 162:C, (1-16), Online publication date: 1-Apr-2022.
- Kordon F, Leuschel M, van de Pol J and Thierry-Mieg Y Software Architecture of Modern Model Checkers Computing and Software Science, (393-419)
- Jensen P, Srba J, Ulrik N and Virenfeldt S Automata-Driven Partial Order Reduction and Guided Search for LTL Model Checking Verification, Model Checking, and Abstract Interpretation, (151-173)
- Garanina N, Anureev I, Zyubin V, Staroletov S, Liakh T, Rozov A and Gorlatch S (2021). A Temporal Logic for Programmable Logic Controllers, Automatic Control and Computer Sciences, 55:7, (763-775), Online publication date: 1-Dec-2021.
- Grompanopoulos C, Gouglidis A and Mavridou A (2021). Specifying and verifying usage control models and policies in TLA, International Journal on Software Tools for Technology Transfer (STTT), 23:5, (685-700), Online publication date: 1-Oct-2021.
- Erbatur S, Schöpp U and Xu C Type-based Enforcement of Infinitary Trace Properties for Java Proceedings of the 23rd International Symposium on Principles and Practice of Declarative Programming, (1-14)
- Horlings E and Jongmans S Analysis of specifications of multiparty sessions with dcj-lint Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, (1590-1594)
- Gnad D, Eisenhut J, Lluch Lafuente A and Hoffmann J Model Checking -Regular Properties with Decoupled Search Computer Aided Verification, (411-434)
- Esparza J Back to the Future: A Fresh Look at Linear Temporal Logic Implementation and Application of Automata, (3-13)
- Kirszenberg A, Martin A, Moreau H and Renault E Go2Pins: A Framework for the LTL Verification of Go Programs Model Checking Software, (140-156)
- Fisher M, Mascardi V, Rozier K, Schlingloff B, Winikoff M and Yorke-Smith N (2020). Towards a framework for certification of reliable autonomous systems, Autonomous Agents and Multi-Agent Systems, 35:1, Online publication date: 1-Apr-2021.
- Aoyama Y, Kuroiwa T and Kushiro N Executable Test Case Generation from Specifications Written in Natural Language and Test Execution Environment 2021 IEEE 18th Annual Consumer Communications & Networking Conference (CCNC), (1-6)
- Nawaz F and Ornik M Explorative Probabilistic Planning with Unknown Target Locations 2020 59th IEEE Conference on Decision and Control (CDC), (2732-2737)
- de Putter S and Wijs A Lock and Fence When Needed: State Space Exploration + Static Analysis = Improved Fence and Lock Insertion Integrated Formal Methods, (297-317)
- Trimananda R, Aqajari S, Chuang J, Demsky B, Xu G and Lu S Understanding and automatically detecting conflicting interactions between smart home IoT applications Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, (1215-1227)
- Gurov D, Hähnle R and Kamburjan E Who Carries the Burden of Modularity? Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles, (3-21)
- von Hippel M, Vick C, Tripakis S and Nita-Rotaru C Automated Attacker Synthesis for Distributed Protocols Computer Safety, Reliability, and Security, (133-149)
- Soethout T, van der Storm T and Vinju J Automated Validation of State-Based Client-Centric Isolation with TLA Software Engineering and Formal Methods. SEFM 2020 Collocated Workshops, (43-57)
- Huang S and Cleaveland R Temporal-Logic Query Checking over Finite Data Streams Formal Methods for Industrial Critical Systems, (252-271)
- Grieco G, Song W, Cygan A, Feist J and Groce A Echidna: effective, usable, and fast fuzzing for smart contracts Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis, (557-560)
- Nath A and Niyogi R Formal Verification of a Distributed Algorithm for Task Execution Computational Science and Its Applications – ICCSA 2020, (120-131)
- Ferrari A, Mazzanti F, Basile D, Beek M and Fantechi A Comparing formal tools for system design Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering, (62-74)
- Konnov I, Lazić M, Stoilkovska I and Widder J Tutorial: Parameterized Verification with Byzantine Model Checker Formal Techniques for Distributed Objects, Components, and Systems, (189-207)
- Kantaros Y and Zavlanos M (2020). STyLuS*, International Journal of Robotics Research, 39:7, (812-836), Online publication date: 1-Jun-2020.
- Nardone R, Marrone S, Gentile U, Amato A, Barberio G, Benerecetti M, De Guglielmo R, Di Martino B, Mazzocca N, Peron A, Pisani G, Velardi L and Vittorini V (2020). An OSLC-based environment for system-level functional testing of ERTMS/ETCS controllers, Journal of Systems and Software, 161:C, Online publication date: 1-Mar-2020.
- Li T, Ye J and Tan Q (2022). Towards functional verifying a family of systemC TLMs, Frontiers of Computer Science: Selected Publications from Chinese Universities, 14:1, (53-66), Online publication date: 1-Feb-2020.
- Tran N A Specification-Based Approach to Model Checking Event-Driven Systems Proceedings of the 10th International Symposium on Information and Communication Technology, (449-456)
- Bajczi L, Vörös A and Molnár V (2019). Will My Program Break on This Faulty Processor?, ACM Transactions on Embedded Computing Systems, 18:5s, (1-21), Online publication date: 31-Oct-2019.
- Vinarskii E, López J, Kushik N, Yevtushenko N and Zeghlache D A Model Checking Based Approach for Detecting SDN Races Testing Software and Systems, (194-211)
- Vukotic I, Rahli V and Esteves-Veríssimo P (2019). Asphalion: trustworthy shielding against Byzantine faults, Proceedings of the ACM on Programming Languages, 3:OOPSLA, (1-32), Online publication date: 10-Oct-2019.
- Gallardo M and Panizo L Teaching Formal Methods: From Software in the Small to Software in the Large Formal Methods Teaching, (97-110)
- Farrell M, Bradbury M, Fisher M, Dennis L, Dixon C, Yuan H and Maple C Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages Software Engineering and Formal Methods, (471-490)
- Shukla N, Pandey M and Srivastava S (2019). Formal modeling and verification of software‐defined networks, International Journal of Network Management, 29:5, Online publication date: 12-Sep-2019.
- Meijer J and van de Pol J (2019). Sound black-box checking in the LearnLib, Innovations in Systems and Software Engineering, 15:3-4, (267-287), Online publication date: 1-Sep-2019.
- Jackson D (2019). Alloy, Communications of the ACM, 62:9, (66-76), Online publication date: 21-Aug-2019.
- Voelter M, Kolb B, Birken K, Tomassetti F, Alff P, Wiart L, Wortmann A and Nordmann A (2019). Using language workbenches and domain-specific languages for safety-critical software development, Software and Systems Modeling (SoSyM), 18:4, (2507-2530), Online publication date: 1-Aug-2019.
- Tran N and Aoki T Conformance Testing of Schedulers for DSL-based Model Checking Model Checking Software, (208-225)
- Tomioka T, Tsunekawa Y and Ueda K Introducing Symmetry to Graph Rewriting Systems with Process Abstraction Graph Transformation, (3-20)
- Pardo R and Le Métayer D Analysis of Privacy Policies to Enhance Informed Consent Data and Applications Security and Privacy XXXIII, (177-198)
- Delporte-Gallet C, Fauconnier H, Jurski Y, Laroussinie F and Sangnier A Towards Synthesis of Distributed Algorithms with SMT Solvers Networked Systems, (200-216)
- Vuotto S, Narizzano M, Pulina L and Tacchella A Automata based test generation with SpecPro Proceedings of the 6th International Workshop on Requirements Engineering and Testing, (13-16)
- Lazreg S, Cordy M, Collet P, Heymans P and Mosser S Multifaceted automated analyses for variability-intensive embedded systems Proceedings of the 41st International Conference on Software Engineering, (854-865)
- Bjørner D (2019). Domain Analysis and Description Principles, Techniques, and Modelling Languages, ACM Transactions on Software Engineering and Methodology, 28:2, (1-67), Online publication date: 9-Apr-2019.
- Rojas E, Doriguzzi-Corin R, Tamurejo S, Beato A, Schwabe A, Phemius K and Guerrero C (2018). Are We Ready to Drive Software-Defined Networks? A Comprehensive Survey on Management Tools and Techniques, ACM Computing Surveys, 51:2, (1-35), Online publication date: 31-Mar-2019.
- Michael E, Woos D, Anderson T, Ernst M and Tatlock Z Teaching Rigorous Distributed Systems With Efficient Model Checking Proceedings of the Fourteenth EuroSys Conference 2019, (1-15)
- Ogata K (2019). A divide & conquer approach to liveness model checking under fairness & anti-fairness assumptions, Frontiers of Computer Science: Selected Publications from Chinese Universities, 13:1, (51-72), Online publication date: 1-Feb-2019.
- Ogunyomi B, Rose L and Kolovos D (2019). Incremental execution of model-to-text transformations using property access traces, Software and Systems Modeling (SoSyM), 18:1, (367-383), Online publication date: 1-Feb-2019.
- Ugawa T, Ritson C and Jones R (2018). Transactional Sapphire, ACM Transactions on Programming Languages and Systems, 40:4, (1-56), Online publication date: 31-Dec-2019.
- Kantaros Y, Johnson B, Chowdhury S, Cappelleri D and Zavlanos M (2018). Control of Magnetic Microrobot Teams for Temporal Micromanipulation Tasks, IEEE Transactions on Robotics, 34:6, (1472-1489), Online publication date: 1-Dec-2018.
- Ozkaya M and Kose M (2018). SAwUML – UML-based, contractual software architectures and their formal analysis using SPIN, Computer Languages, Systems and Structures, 54:C, (71-94), Online publication date: 1-Dec-2018.
- Konnov I and Widder J ByMC: Byzantine Model Checker Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems, (327-342)
- Desai A, Qadeer S and Seshia S Programming Safe Robotics Systems: Challenges and Advances Leveraging Applications of Formal Methods, Verification and Validation. Verification, (103-119)
- Bu L, Peled D, Shen D and Tzirulnikov Y Chasing Errors Using Biasing Automata Leveraging Applications of Formal Methods, Verification and Validation. Verification, (271-286)
- Eljadiri L, Assayad I and Zakari A Generic Verification of Safety Properties For SystemC Programs Using Incomplete Interactions Proceedings of the 2nd International Conference on Smart Digital Environment, (166-171)
- Bošnaă?Ki D and Wijs A (2018). Model checking, International Journal on Software Tools for Technology Transfer (STTT), 20:5, (493-497), Online publication date: 1-Oct-2018.
- Edelkamp S and Greulich C (2018). A case study of planning for smart factories, International Journal on Software Tools for Technology Transfer (STTT), 20:5, (515-528), Online publication date: 1-Oct-2018.
- Gallardo M, Merino P, Panizo L and Salmerón A (2018). Integrating river basin DSSs with model checking, International Journal on Software Tools for Technology Transfer (STTT), 20:5, (499-514), Online publication date: 1-Oct-2018.
- Nardone R, De Tommasi G, Mazzocca N, Pironti A and Vittorini V Automatic generation of formal models for diagnosability of DES 2018 IEEE 23rd International Conference on Emerging Technologies and Factory Automation (ETFA), (43-48)
- Beyer D and Friedberger K Domain-independent multi-threaded software model checking Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, (634-644)
- Alzahrani M and Georgieva L Structural modeling and verification of web applications Proceedings of the 8th International Conference on Web Intelligence, Mining and Semantics, (1-4)
- Kordon F and Thierry-Mieg Y Self-adaptive Model Checking, the Next Step? Application and Theory of Petri Nets and Concurrency, (3-15)
- Mazzanti F, Ferrari A and Spagnolo G (2018). Towards formal methods diversity in railways, International Journal on Software Tools for Technology Transfer (STTT), 20:3, (263-288), Online publication date: 1-Jun-2018.
- Naujokat S, Lybecait M, Kopetzki D and Steffen B (2018). CINCO, International Journal on Software Tools for Technology Transfer (STTT), 20:3, (327-354), Online publication date: 1-Jun-2018.
- Groce A, Holmes J, Marinov D, Shi A and Zhang L An extensible, regular-expression-based tool for multi-language mutant generation Proceedings of the 40th International Conference on Software Engineering: Companion Proceeedings, (25-28)
- Degiovanni R, Castro P, Arroyo M, Ruiz M, Aguirre N and Frias M Goal-conflict likelihood assessment based on model counting Proceedings of the 40th International Conference on Software Engineering, (1125-1135)
- Leupolz J, Habermaier A and Reif W (2018). Quantitative and qualitative safety analysis of a hemodialysis machine with S#, Journal of Software: Evolution and Process, 30:5, Online publication date: 17-May-2018.
- Flittner M, Mahfoudi M, Saucez D, Wählisch M, Iannone L, Bajpai V and Afanasyev A (2018). A Survey on Artifacts from CoNEXT, ICN, IMC, and SIGCOMM Conferences in 2017, ACM SIGCOMM Computer Communication Review, 48:1, (75-80), Online publication date: 27-Apr-2018.
- Tran N, Chiba Y and Aoki T Qualitative and quantitative analysis with scheduling policies in model checking Proceedings of the 33rd Annual ACM Symposium on Applied Computing, (1873-1880)
- Bai X, Cheng Z, Duan Z and Hu K Formal Modeling and Verification of Smart Contracts Proceedings of the 2018 7th International Conference on Software and Computer Applications, (322-326)
- Prasetya I (2018). Temporal algebraic query of test sequences, Journal of Systems and Software, 136:C, (223-236), Online publication date: 1-Feb-2018.
- Holmes J, Groce A, Pinto J, Mittal P, Azimi P, Kellar K and O'brien J (2018). TSTL, International Journal on Software Tools for Technology Transfer (STTT), 20:1, (57-78), Online publication date: 1-Feb-2018.
- Wang K, Khurshid S and Gligoric M (2018). JPR, ACM SIGSOFT Software Engineering Notes, 42:4, (1-5), Online publication date: 11-Jan-2018.
- Dimovski A (2018). Verifying annotated program families using symbolic game semantics, Theoretical Computer Science, 706:C, (35-53), Online publication date: 6-Jan-2018.
- Gularte A, Mendizabal O, Barbosa R and Adamatti D (2018). Node and Link Allocation in Network Virtualization Based on Distributed Constraint Optimization, Journal of Network and Systems Management, 26:1, (127-146), Online publication date: 1-Jan-2018.
- Brunner J and Lammich P (2018). Formal Verification of an Executable LTL Model Checker with Partial Order Reduction, Journal of Automated Reasoning, 60:1, (3-21), Online publication date: 1-Jan-2018.
- Alvaro P and Tymon S (2017). Abstracting the geniuses away from failure testing, Communications of the ACM, 61:1, (54-61), Online publication date: 27-Dec-2017.
- Harbouche A, Djedi N, Erradi M, Ben-Othman J and Kobbane A (2017). Model driven flexible design of a wireless body sensor network for health monitoring, Computer Networks: The International Journal of Computer and Telecommunications Networking, 129:P2, (548-571), Online publication date: 24-Dec-2017.
- Li Y, Deutsch A and Vianu V (2017). VERIFAS, Proceedings of the VLDB Endowment, 11:3, (283-296), Online publication date: 1-Nov-2017.
- Santos J, Zahn J, Silvestre E, Silva V and Vasconcelos W (2017). Detection and resolution of normative conflicts in multi-agent systems, Autonomous Agents and Multi-Agent Systems, 31:6, (1236-1282), Online publication date: 1-Nov-2017.
- Lucia A, Deufemia V, Gravino C and Risi M (2018). Detecting the Behavior of Design Patterns through Model Checking and Dynamic Analysis, ACM Transactions on Software Engineering and Methodology, 26:4, (1-41), Online publication date: 31-Oct-2017.
- Ou P and Demsky B (2017). Checking Concurrent Data Structures Under the C/C++11 Memory Model, ACM SIGPLAN Notices, 52:8, (45-59), Online publication date: 26-Oct-2017.
- Baresi L, Morzenti A, Motta A, K. M and Rossi M (2017). A Logic-Based Approach for the Verification of UML Timed Models, ACM Transactions on Software Engineering and Methodology, 26:2, (1-47), Online publication date: 5-Oct-2017.
- Brau G, Navet N and Hugues J Heterogeneous models and analyses in the design of real-time embedded systems - an avionic case-study Proceedings of the 25th International Conference on Real-Time Networks and Systems, (168-177)
- Mudduluru R, Deligiannis P, Desai A, Lal A and Qadeer S Lasso detection using partial-state caching Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design, (84-91)
- Dimovski A, Al-Sibahi A, Brabrand C and Wąsowski A (2017). Efficient family-based model checking via variability abstractions, International Journal on Software Tools for Technology Transfer (STTT), 19:5, (585-603), Online publication date: 1-Oct-2017.
- Pal D, Vain J, Srinivasan S and Ramaswamy S Model-based maintenance scheduling in flexible modular automation systems 2017 22nd IEEE International Conference on Emerging Technologies and Factory Automation (ETFA), (1-6)
- Kamide N and Yano R (2017). Logics and translations for hierarchical model checking, Procedia Computer Science, 112:C, (31-40), Online publication date: 1-Sep-2017.
- Kumar A and Pais A (2017). En-Route Filtering Techniques in Wireless Sensor Networks, Wireless Personal Communications: An International Journal, 96:1, (697-739), Online publication date: 1-Sep-2017.
- Panizo L, Salmerón A, Gallardo M and Merino P Guided test case generation for mobile apps in the TRIANGLE project: work in progress Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, (192-195)
- Moszkowski B and Guelev D (2017). An application of temporal projection to interleaving concurrency, Formal Aspects of Computing, 29:4, (705-750), Online publication date: 1-Jul-2017.
- Wu M, Zeng H, Wang C and Yu H Safety Guard Proceedings of the 54th Annual Design Automation Conference 2017, (1-6)
- Yacoub A, Hamri M and Frydman C Restricting DEv-PROMELA with a hierarchy of simulation formalisms Proceedings of the Symposium on Theory of Modeling & Simulation, (1-11)
- Dimovski A and Wąsowski A Variability-Specific Abstraction Refinement for Family-Based Model Checking Proceedings of the 20th International Conference on Fundamental Approaches to Software Engineering - Volume 10202, (406-423)
- Di Pompeo D, Incerto E, Muttillo V, Pomante L and Valenete G An Efficient Performance-Driven Approach for HW/SW Co-Design Proceedings of the 8th ACM/SPEC on International Conference on Performance Engineering, (323-326)
- Valmari A (2017). Stop It, and Be Stubborn!, ACM Transactions on Embedded Computing Systems, 16:2, (1-26), Online publication date: 14-Apr-2017.
- Qiu Y, Ma M and Wang X (2017). A proxy signature-based handover authentication scheme for LTE wireless networks, Journal of Network and Computer Applications, 83:C, (63-71), Online publication date: 1-Apr-2017.
- (2017). State space search nogood learning, Artificial Intelligence, 245:C, (1-37), Online publication date: 1-Apr-2017.
- Alur R and Tripakis S (2017). Automatic Synthesis of Distributed Protocols, ACM SIGACT News, 48:1, (55-90), Online publication date: 10-Mar-2017.
- Wang H and Zhang T (2017). Software model checking for resources race, Cluster Computing, 20:1, (179-193), Online publication date: 1-Mar-2017.
- Karimi V, Alencar P and Cowan D (2017). A formal modeling and analysis approach for access control rules, policies, and their combinations, International Journal of Information Security, 16:1, (43-74), Online publication date: 1-Feb-2017.
- Ou P and Demsky B Checking Concurrent Data Structures Under the C/C++11 Memory Model Proceedings of the 22nd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, (45-59)
- Konnov I, Lazić M, Veith H and Widder J A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, (719-734)
- Borchert C, Schirmeier H and Spinczyk O (2017). Generic Soft-Error Detection and Correction for Concurrent Data Structures, IEEE Transactions on Dependable and Secure Computing, 14:1, (22-36), Online publication date: 1-Jan-2017.
- Li W, Mani R and Mosterman P Extensible discrete-event simulation framework in simevents Proceedings of the 2016 Winter Simulation Conference, (943-954)
- Huang S and Huang J (2016). Maximal causality reduction for TSO and PSO, ACM SIGPLAN Notices, 51:10, (447-461), Online publication date: 5-Dec-2016.
- Khalili A, Narizzano M and Tacchella A Learning for Verification in Embedded Systems: A Case Study AI*IA 2016 Advances in Artificial Intelligence, (525-538)
- Ren Z and Xi H Combining type-checking with model-checking for system verification Proceedings of the 14th ACM-IEEE International Conference on Formal Methods and Models for System Design, (54-58)
- Zhang H and Lu Y SMT-based Bounded Model Checking for Cooperative Software with a Deterministic Scheduler 6th International Workshop on Structured Object-Oriented Formal Language and Method - Volume 10189, (181-200)
- Bérard B, Lafourcade P, Millet L, Potop-Butucaru M, Thierry-Mieg Y and Tixeuil S (2016). Formal verification of mobile robot protocols, Distributed Computing, 29:6, (459-487), Online publication date: 1-Nov-2016.
- Kirwan R, Miller A and Porr B (2016). Model checking learning agent systems using Promela with embedded C code and abstraction, Formal Aspects of Computing, 28:6, (1027-1056), Online publication date: 1-Nov-2016.
- Mayer M and Madhavan R A Scala library for testing student assignments on concurrent programming Proceedings of the 2016 7th ACM SIGPLAN Symposium on Scala, (1-10)
- Huang S and Huang J Maximal causality reduction for TSO and PSO Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, (447-461)
- Alvaro P, Andrus K, Sanden C, Rosenthal C, Basiri A and Hochstein L Automating Failure Testing Research at Internet Scale Proceedings of the Seventh ACM Symposium on Cloud Computing, (17-28)
- Muschevici R, Proença J and Clarke D (2016). Feature Nets, Software and Systems Modeling (SoSyM), 15:4, (1181-1206), Online publication date: 1-Oct-2016.
- Santos I, Rocha L, Neto P and Andrade R Model Verification of Dynamic Software Product Lines Proceedings of the XXX Brazilian Symposium on Software Engineering, (113-122)
- Olaechea R, Fahrenberg U, Atlee J and Legay A Long-term average cost in featured transition systems Proceedings of the 20th International Systems and Software Product Line Conference, (109-118)
- Almagor S, Boker U and Kupferman O (2016). Formally Reasoning About Quality, Journal of the ACM, 63:3, (1-56), Online publication date: 1-Sep-2016.
- Qu H and Veres S (2016). Verification of logical consistency in robotic reasoning, Robotics and Autonomous Systems, 83:C, (44-56), Online publication date: 1-Sep-2016.
- Dardaillon M, Marquet K, Risset T, Martin J and Charles H (2016). A New Compilation Flow for Software-Defined Radio Applications on Heterogeneous MPSoCs, ACM Transactions on Architecture and Code Optimization, 13:2, (1-25), Online publication date: 27-Jun-2016.
- Brunner J and Lammich P Formal Verification of an Executable LTL Model Checker with Partial Order Reduction Proceedings of the 8th International Symposium on NASA Formal Methods - Volume 9690, (307-321)
- Raimondi F (2016). Using multi-agent systems to go beyond temporal patterns verification, ACM SIGLOG News, 3:2, (69-77), Online publication date: 31-May-2016.
- Kossak F and Mashkoor A How to Select the Suitable Formal Method forźan Industrial Application Proceedings of the 5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z - Volume 9675, (213-228)
- Yacoub A, Hamri M and Frydman C Using DEv-PROMELA for Modelling and Verification of Software Proceedings of the 2016 ACM SIGSIM Conference on Principles of Advanced Discrete Simulation, (245-253)
- Wang Y and Wagner S Towards applying a safety analysis and verification method based on STPA to agile software development Proceedings of the International Workshop on Continuous Software Evolution and Delivery, (5-11)
- Norris B and Demsky B (2016). A Practical Approach for Model Checking C/C++11 Code, ACM Transactions on Programming Languages and Systems, 38:3, (1-51), Online publication date: 2-May-2016.
- Jančík P and Kofroň J Dead variable analysis for multi-threaded heap manipulating programs Proceedings of the 31st Annual ACM Symposium on Applied Computing, (1620-1627)
- Maiya P, Gupta R, Kanade A and Majumdar R Partial Order Reduction for Event-Driven Multi-threaded Programs Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 9636, (680-697)
- Armando A, Carbone R and Compagna L (2016). SATMC, International Journal on Software Tools for Technology Transfer (STTT), 18:2, (187-204), Online publication date: 1-Apr-2016.
- Gibson-Robinson T, Armstrong P, Boulgakov A and Roscoe A (2016). FDR3, International Journal on Software Tools for Technology Transfer (STTT), 18:2, (149-167), Online publication date: 1-Apr-2016.
- Ramanathan A, Pullum L, Hussain F, Chakrabarty D and Jha S Integrating symbolic and statistical methods for testing intelligent systems applications to machine learning and computer vision Proceedings of the 2016 Conference on Design, Automation & Test in Europe, (786-791)
- Vekris D, Lang F, Dima C and Mateescu R (2016). Verification of specifications using CADP, Formal Aspects of Computing, 28:1, (145-178), Online publication date: 1-Mar-2016.
- Holzmann G Cloud-Based Verification of Concurrent Software Proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 9583, (311-327)
- Demsky B and Lam P (2015). SATCheck: SAT-directed stateless model checking for SC and TSO, ACM SIGPLAN Notices, 50:10, (20-36), Online publication date: 18-Dec-2015.
- Park H, Malik A and Salcic Z (2015). Compiling and verifying SC-SystemJ programs for safety-critical reactive systems, Computer Languages, Systems and Structures, 44:PC, (251-282), Online publication date: 1-Dec-2015.
- Moszkowski B and Guelev D An Application of Temporal Projection toźInterleaving Concurrency Proceedings of the First International Symposium on Dependable Software Engineering: Theories, Tools, and Applications - Volume 9409, (153-167)
- Kamkin A (2015). Projecting transition systems, Programming and Computing Software, 41:6, (311-324), Online publication date: 1-Nov-2015.
- Dabaghchian M and Abdollahi Azgomi M (2015). Model checking the observational determinism security property using PROMELA and SPIN, Formal Aspects of Computing, 27:5-6, (789-804), Online publication date: 1-Nov-2015.
- Demsky B and Lam P SATCheck: SAT-directed stateless model checking for SC and TSO Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, (20-36)
- Štill V, RoăźKai P and Barnat J Weak Memory Models as LLVM-to-LLVM Transformations Revised Selected Papers of the 10th International Doctoral Workshop on Mathematical and Engineering Methods in Computer Science - Volume 9548, (144-155)
- Jafari Navimipour N (2015). A formal approach for the specification and verification of a Trustworthy Human Resource Discovery mechanism in the Expert Cloud, Expert Systems with Applications: An International Journal, 42:15, (6112-6131), Online publication date: 1-Sep-2015.
- Arcaini P, Gargantini A and Riccobene E Improving model-based test generation by model decomposition Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, (119-130)
- Michaud T and Duret-Lutz A Practical Stutter-Invariance Checks for $$\omega $$-Regular Languages Proceedings of the 22nd International Symposium on Model Checking Software - Volume 9232, (84-101)
- Blahoudek F, Duret-Lutz A, Rujbr V and StrejăźEk J On Refinement of Büchi Automata for Explicit Model Checking Proceedings of the 22nd International Symposium on Model Checking Software - Volume 9232, (66-83)
- Dimovski A, Al-Sibahi A, Brabrand C and Wąsowski A Family-Based Model Checking Without a Family-Based Model Checker Proceedings of the 22nd International Symposium on Model Checking Software - Volume 9232, (282-299)
- Beer A, Heidinger S, Kühne U, Leitner-Fischer F and Leue S Symbolic Causality Checking Using Bounded Model Checking Proceedings of the 22nd International Symposium on Model Checking Software - Volume 9232, (203-221)
- Longfield S, Nkounkou B, Manohar R and Tate R (2015). Preventing glitches and short circuits in high-level self-timed chip specifications, ACM SIGPLAN Notices, 50:6, (270-279), Online publication date: 7-Aug-2015.
- Dimovski A, Al-Sibahi A, Brabrand C and Wąsowski A Family-based model checking using off-the-shelf model checkers Proceedings of the 19th International Conference on Software Product Line, (397-397)
- Stievenart Q, Nicolay J, De Meuter W and De Roover C Detecting concurrency bugs in higher-order programs through abstract interpretation Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, (232-243)
- Groce A, Pinto J, Azimi P and Mittal P TSTL: a language and tool for testing (demo) Proceedings of the 2015 International Symposium on Software Testing and Analysis, (414-417)
- Sato Y, Hozumi S and Chiba S Calculation coverage testing in scientific applications Proceedings of the 2015 International Symposium on Software Testing and Analysis, (350-360)
- Longfield S, Nkounkou B, Manohar R and Tate R Preventing glitches and short circuits in high-level self-timed chip specifications Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, (270-279)
- Alvaro P, Rosen J and Hellerstein J Lineage-driven Fault Injection Proceedings of the 2015 ACM SIGMOD International Conference on Management of Data, (331-346)
- Huang K, Yu M, Yan R, Zhang X, Yan X, Brisolara L, Jerraya A and Feng J (2015). Communication Optimizations for Multithreaded Code Generation from Simulink Models, ACM Transactions on Embedded Computing Systems, 14:3, (1-26), Online publication date: 21-May-2015.
- Qian J, Liu J, Chen X and Sun J Modeling and verification of zone controller Proceedings of the First International Workshop on Complex faUlts and Failures in LargE Software Systems, (48-54)
- van den Berghe A Towards a practical security analysis methodology Proceedings of the 37th International Conference on Software Engineering - Volume 2, (883-886)
- Park Y, Hong S, Kim M, Lee D and Cho J Systematic testing of reactive software with non-deterministic events Proceedings of the 37th International Conference on Software Engineering - Volume 2, (29-38)
- Ugawa T, Jones R and Ritson C (2014). Reference object processing in on-the-fly garbage collection, ACM SIGPLAN Notices, 49:11, (59-69), Online publication date: 11-May-2015.
- Abdulla P, Atig M and Ngo T The Best of Both Worlds Proceedings of the 24th European Symposium on Programming on Programming Languages and Systems - Volume 9032, (308-332)
- Jafari Navimipour N, Habibizad Navin A, Rahmani A and Hosseinzadeh M (2015). Behavioral modeling and automated verification of a Cloud-based framework to share the knowledge and skills of human resources, Computers in Industry, 68:C, (65-77), Online publication date: 1-Apr-2015.
- Armando A, Costa G, Merlo A and Verderame L (2015). Formal modeling and automatic enforcement of Bring Your Own Device policies, International Journal of Information Security, 14:2, (123-140), Online publication date: 1-Apr-2015.
- Buhr P, Dice D and Hesselink W (2015). High-performance N-thread software solutions for mutual exclusion, Concurrency and Computation: Practice & Experience, 27:3, (651-701), Online publication date: 10-Mar-2015.
- Chen Z, Zhang D and Ma Y (2015). Modeling and analyzing the convergence property of the BGP routing protocol in SPIN, Telecommunications Systems, 58:3, (205-217), Online publication date: 1-Mar-2015.
- Vizovitin N, Nepomniaschy V and Stenenko A (2015). Verifying UCM Specifications of Distributed Systems Using Colored Petri Nets, Cybernetics and Systems Analysis, 51:2, (213-222), Online publication date: 1-Mar-2015.
- Zave P (2015). A practical comparison of Alloy and Spin, Formal Aspects of Computing, 27:2, (239-253), Online publication date: 1-Mar-2015.
- Gligoric M, Schulte W, Prasad C, van Velzen D, Narasamdya I and Livshits B (2014). Automated migration of build scripts using dynamic analysis and search-based refactoring, ACM SIGPLAN Notices, 49:10, (599-616), Online publication date: 31-Dec-2015.
- Bocchino R, Gamble E, Gostelow K and Some R (2014). Spot, ACM SIGAda Ada Letters, 34:3, (97-102), Online publication date: 26-Nov-2014.
- Cordy M, Heymans P, Legay A, Schobbens P, Dawagne B and Leucker M Counterexample guided abstraction refinement of product-line behavioural models Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, (190-201)
- Longfield S and Manohar R Removing concurrency for rapid functional verification Proceedings of the 2014 IEEE/ACM International Conference on Computer-Aided Design, (332-339)
- Arcaini P and Gargantini A (2014). Test generation for sequential nets of Abstract State Machines with information passing, Science of Computer Programming, 94:P2, (93-108), Online publication date: 1-Nov-2014.
- Bocchino R, Gamble E, Gostelow K and Some R Spot Proceedings of the 2014 ACM SIGAda annual conference on High integrity language technology, (97-102)
- Gligoric M, Schulte W, Prasad C, van Velzen D, Narasamdya I and Livshits B Automated migration of build scripts using dynamic analysis and search-based refactoring Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, (599-616)
- Naujokat S, Traonouez L, Isberner M, Steffen B and Legay A Domain-Specific Code Generator Modeling Part I of the Proceedings of the 6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change - Volume 8802, (481-498)
- Permpoontanalarp Y and Sornkhom P (2014). On-the-fly Trace Generation Approach to the Security Analysis of Cryptographic Protocols, Fundamenta Informaticae, 130:4, (423-466), Online publication date: 1-Oct-2014.
- From visual to logical formalisms for SoC validation Proceedings of the Twelfth ACM/IEEE Conference on Formal Methods and Models for Codesign, (165-174)
- Yacoub A, Hamri M and Frydman C A Method for Improving the Verification and Validation of Systems by the Combined Use of Simulation and Formal Methods Proceedings of the 2014 IEEE/ACM 18th International Symposium on Distributed Simulation and Real Time Applications, (155-162)
- Cordy M, Willemart M, Dawagne B, Heymans P and Schobbens P An extensible platform for product-line behavioural analysis Proceedings of the 18th International Software Product Line Conference: Companion Volume for Workshops, Demonstrations and Tools - Volume 2, (102-109)
- Basu S and Bultan T Automatic verification of interactions in asynchronous systems with unbounded buffers Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering, (743-754)
- Zhou R, Li C, Min R, Yu Q, Gu F, Zhou Q, Hung J, Li K and Wang X (2014). On design and formal verification of SNSP, The Journal of Supercomputing, 69:3, (1254-1283), Online publication date: 1-Sep-2014.
- Ruys T Unit testing for SPIN: runspin and parsepan Proceedings of the 2014 International SPIN Symposium on Model Checking of Software, (133-136)
- Brezočnik Z, Vlaovič B and Vreže A SpinRCP: the eclipse rich client platform integrated development environment for the spin model checker Proceedings of the 2014 International SPIN Symposium on Model Checking of Software, (125-128)
- Blahoudek F, Duret-Lutz A, Křetínský M and Strejček J Is there a best büchi automaton for explicit model checking? Proceedings of the 2014 International SPIN Symposium on Model Checking of Software, (68-76)
- Leitner-Fischer F and Leue S SpinCause: a tool for causality checking Proceedings of the 2014 International SPIN Symposium on Model Checking of Software, (117-120)
- Shacham O, Yahav E, Gueta G, Aiken A, Bronson N, Sagiv M and Vechev M Verifying atomicity via data independence Proceedings of the 2014 International Symposium on Software Testing and Analysis, (26-36)
- Gmeiner A, Konnov I, Schmid U, Veith H and Widder J Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms Advanced Lectures of the 14th International School on Formal Methods for Executable Software Models - Volume 8483, (122-171)
- Ugawa T, Jones R and Ritson C Reference object processing in on-the-fly garbage collection Proceedings of the 2014 international symposium on Memory management, (59-69)
- Visser W, Bjørner N and Shankar N Software engineering and automated deduction Future of Software Engineering Proceedings, (155-166)
- Amani S, Chubb P, Donaldson A, Legg A, Ong K, Ryzhyk L and Zhu Y (2014). Automatic verification of active device drivers, ACM SIGOPS Operating Systems Review, 48:1, (106-118), Online publication date: 15-May-2014.
- BjØrner D and Havelund K 40 Years of Formal Methods Proceedings of the 19th International Symposium on FM 2014: Formal Methods - Volume 8442, (42-61)
- Helmert M, Haslum P, Hoffmann J and Nissim R (2014). Merge-and-Shrink Abstraction, Journal of the ACM, 61:3, (1-63), Online publication date: 1-May-2014.
- Adalid D, Salmerón A, Gallardo M and Merino P (2014). Using SPIN for automated debugging of infinite executions of Java programs, Journal of Systems and Software, 90:C, (61-75), Online publication date: 1-Apr-2014.
- Moscato M, Pombo C and Frias M (2014). Dynamite, ACM Transactions on Software Engineering and Methodology, 23:2, (1-37), Online publication date: 1-Mar-2014.
- Classen A, Cordy M, Heymans P, Legay A and Schobbens P (2014). Formal semantics, modular specification, and symbolic verification of product-line behaviour, Science of Computer Programming, 80:PB, (416-439), Online publication date: 1-Feb-2014.
- Holzmann G (2014). Mars code, Communications of the ACM, 57:2, (64-73), Online publication date: 1-Feb-2014.
- Jezequel L and Esparza J Message-Passing Algorithms for the Verification of Distributed Protocols Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 8318, (222-241)
- Deng D, Zhang W and Lu S (2013). Efficient concurrency-bug detection across inputs, ACM SIGPLAN Notices, 48:10, (785-802), Online publication date: 12-Nov-2013.
- Norris B and Demsky B (2013). CDSchecker, ACM SIGPLAN Notices, 48:10, (131-150), Online publication date: 12-Nov-2013.
- Deng D, Zhang W and Lu S Efficient concurrency-bug detection across inputs Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications, (785-802)
- Norris B and Demsky B CDSchecker Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications, (131-150)
- Yang H, Cai C, Peng L, Zhao X, Qiu Z and Qin S (2013). Algorithms for checking channel passing in web service choreography, Frontiers of Computer Science: Selected Publications from Chinese Universities, 7:5, (710-728), Online publication date: 1-Oct-2013.
- Ern B, Nguyen V and Noll T Characterization of Failure Effects on AADL Models Proceedings of the 32nd International Conference on Computer Safety, Reliability, and Security - Volume 8153, (241-252)
- Randolph A, Imine A, Boucheneb H and Quintero A Specification and Verification Using Alloy of Optimistic Access Control for Distributed Collaborative Editors Proceedings of the 18th International Workshop on Formal Methods for Industrial Critical Systems - Volume 8187, (184-198)
- Bonacchi A, Fantechi A, Bacherini S, Tempestini M and Cipriani L Validation of Railway Interlocking Systems by Formal Verification, A Case Study Revised Selected Papers of the SEFM 2013 Collocated Workshops on Software Engineering and Formal Methods - Volume 8368, (237-252)
- Dennis L, Fisher M and Webster M Using Agent JPF to Build Models for Other Model Checkers Proceedings of the 14th International Workshop on Computational Logic in Multi-Agent Systems - Volume 8143, (273-289)
- Latella D, Loreti M and Massink M On-the-fly Fast Mean-Field Model-Checking 8th International Symposium on Trustworthy Global Computing - Volume 8358, (297-314)
- Adzkiya D and Abate A VeriSiMPL Proceedings of the 10th international conference on Quantitative Evaluation of Systems, (274-277)
- Cordy M, Classen A, Heymans P, Schobbens P and Legay A ProVeLines Proceedings of the 17th International Software Product Line Conference co-located workshops, (141-146)
- Dong R, Faber J, Ke W and Liu Z rCOS Unifying Theories of Programming and Formal Engineering Methods, (1-66)
- McPeak S, Gros C and Ramanathan M Scalable and incremental software bug detection Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, (554-564)
- Nelson T, Guha A, Dougherty D, Fisler K and Krishnamurthi S A balance of power Proceedings of the second ACM SIGCOMM workshop on Hot topics in software defined networking, (79-84)
- Desnoyers M, McKenney P and Dagenais M (2013). Multi-core systems modeling for formal verification of parallel algorithms, ACM SIGOPS Operating Systems Review, 47:2, (51-65), Online publication date: 23-Jul-2013.
- Bonacchi A Formal safety proof: a real case study in a railway interlocking system Proceedings of the 2013 International Symposium on Software Testing and Analysis, (378-381)
- Esparza J, Lammich P, Neumann R, Nipkow T, Schimpf A and Smaus J A Fully Verified Executable LTL Model Checker Proceedings of the 25th International Conference on Computer Aided Verification - Volume 8044, (463-478)
- Tsai M, Tsay Y and Hwang Y GOAL for Games, Omega-Automata, and Logics Proceedings of the 25th International Conference on Computer Aided Verification - Volume 8044, (883-889)
- Udupa A, Raghavan A, Deshmukh J, Mador-Haim S, Martin M and Alur R (2013). TRANSIT, ACM SIGPLAN Notices, 48:6, (287-296), Online publication date: 23-Jun-2013.
- Udupa A, Raghavan A, Deshmukh J, Mador-Haim S, Martin M and Alur R TRANSIT Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, (287-296)
- Xu G, Li W, Xu R, Xiao Y, Gao H, Li X, Feng Z and Mei J (2013). An algorithm on fairness verification of mobile sink routing in wireless sensor network, Personal and Ubiquitous Computing, 17:5, (851-864), Online publication date: 1-Jun-2013.
- Bąk K, Zayan D, Czarnecki K, Antkiewicz M, Diskin Z, Wąsowski A and Rayside D Example-driven modeling: model = abstractions + examples Proceedings of the 2013 International Conference on Software Engineering, (1273-1276)
- Cordy M, Schobbens P, Heymans P and Legay A Beyond boolean product-line model checking: dealing with feature attributes and multi-features Proceedings of the 2013 International Conference on Software Engineering, (472-481)
- Zave P and Rexford J Compositional Network Mobility Revised Selected Papers of the 5th International Conference on Verified Software: Theories, Tools, Experiments - Volume 8164, (68-87)
- Hunter J, Raimondi F, Rungta N and Stocker R A synergistic and extensible framework for multi-agent system verification Proceedings of the 2013 international conference on Autonomous agents and multi-agent systems, (869-876)
- Skowyra R, Lapets A, Bestavros A and Kfoury A Verifiably-safe software-defined networks for CPS Proceedings of the 2nd ACM international conference on High confidence networked systems, (101-110)
- Tsay Y, Tsai M, Chang J, Chang Y and Liu C (2013). Büchi Store, International Journal on Software Tools for Technology Transfer (STTT), 15:2, (109-123), Online publication date: 1-Apr-2013.
- Garavel H, Lang F, Mateescu R and Serwe W (2013). CADP 2011, International Journal on Software Tools for Technology Transfer (STTT), 15:2, (89-107), Online publication date: 1-Apr-2013.
- Hildebrandt T, Mukkamala R, Slaats T and Zanitti F Modular context-sensitive and aspect-oriented processes with dynamic condition response graphs Proceedings of the 12th workshop on Foundations of aspect-oriented languages, (19-24)
- She Y, Li H and Zhu H UVHM Proceedings of the 2013 international conference on Information and Communication Technology, (300-305)
- Renault E, Duret-Lutz A, Kordon F and Poitrenaud D Strength-Based decomposition of the property Büchi automaton for faster model checking Proceedings of the 19th international conference on Tools and Algorithms for the Construction and Analysis of Systems, (580-593)
- Linden A and Wolper P A verification-based approach to memory fence insertion in PSO memory systems Proceedings of the 19th international conference on Tools and Algorithms for the Construction and Analysis of Systems, (339-353)
- Cranen S, Groote J, Keiren J, Stappers F, de Vink E, Wesselink W and Willemse T An overview of the mCRL2 toolset and its recent advances Proceedings of the 19th international conference on Tools and Algorithms for the Construction and Analysis of Systems, (199-213)
- Murray T (2013). On the limits of refinement-testing for model-checking CSP, Formal Aspects of Computing, 25:2, (219-256), Online publication date: 1-Mar-2013.
- Sun J, Liu Y, Dong J, Liu Y, Shi L and André É (2013). Modeling and verifying hierarchical real-time systems using stateful timed CSP, ACM Transactions on Software Engineering and Methodology, 22:1, (1-29), Online publication date: 1-Feb-2013.
- Wright A (2013). Revving the rover, Communications of the ACM, 56:2, (14-16), Online publication date: 1-Feb-2013.
- Leitner-Fischer F and Leue S Causality Checking for Complex System Models Proceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 7737, (248-267)
- Mouradian A and Augé-Blum I Modeling local broadcast behavior of wireless sensor networks with timed automata for model checking of WCTT Proceeings of the 2nd International Workshop on Worst-Case Traversal Time, (23-30)
- Zave P and Rexford J The geomorphic view of networking Proceedings of the 7th Workshop on Middleware for Next Generation Internet Computing, (1-6)
- Ogata K and Thi Thanh Huyen P Specification and model checking of the chandy and lamport distributed snapshot algorithm in rewriting logic Proceedings of the 14th international conference on Formal Engineering Methods: formal methods and software engineering, (87-102)
- Shi L, Liu Y, Sun J, Dong J and Carvalho G An analytical and experimental comparison of CSP extensions and tools Proceedings of the 14th international conference on Formal Engineering Methods: formal methods and software engineering, (381-397)
- Rozier K and Vardi M Deterministic compilation of temporal safety properties in explicit state model checking Proceedings of the 8th international conference on Hardware and Software: verification and testing, (243-259)
- Marques E, Balegas V, Barroca B, Barisic A and Amaral V The RPG DSL Proceedings of the 2012 workshop on Domain-specific modeling, (13-18)
- McKenney P Beyond expert-only parallel programming? Proceedings of the 2012 ACM workshop on Relaxing synchronization for multicore and manycore scalability, (25-32)
- Fourie J, Geldenhuys J and Inggs C Improving communication for distributed model checking Proceedings of the South African Institute for Computer Scientists and Information Technologists Conference, (41-50)
- Classen A, Cordy M, Heymans P, Legay A and Schobbens P (2012). Model checking software product lines with SNIP, International Journal on Software Tools for Technology Transfer (STTT), 14:5, (589-612), Online publication date: 1-Oct-2012.
- Stocker R, Dennis L, Dixon C and Fisher M Verifying brahms human-robot teamwork models Proceedings of the 13th European conference on Logics in Artificial Intelligence, (385-397)
- Yatake K and Aoki T Model checking of OSEK/VDX OS design model based on environment modeling Proceedings of the 9th international conference on Theoretical Aspects of Computing, (183-197)
- Braz F, Cruz J, Faria-Campos A and Campos S Palytoxin inhibits the sodium-potassium pump --- an investigation of an electrophysiological model using probabilistic model checking Proceedings of the 15th Brazilian conference on Formal Methods: foundations and applications, (35-50)
- Bolis F, Gargantini A, Guarnieri M, Magri E and Musto L Model-Driven testing for web applications using abstract state machines Proceedings of the 12th international conference on Current Trends in Web Engineering, (71-78)
- Leue S and Tabaei Befrouei M Counterexample explanation by anomaly detection Proceedings of the 19th international conference on Model Checking Software, (24-42)
- Jiang Y and Qiu Z S2N Proceedings of the 19th international conference on Model Checking Software, (255-260)
- Sulzmann M and Zechner A Model checking DSL-generated c source code Proceedings of the 19th international conference on Model Checking Software, (241-247)
- Zeng R, Sun Z, Liu S and He X McPatom Proceedings of the 19th international conference on Model Checking Software, (191-207)
- Burns E and Zhou R Parallel model checking using abstraction Proceedings of the 19th international conference on Model Checking Software, (172-190)
- Holzmann G Parallelizing the spin model checker Proceedings of the 19th international conference on Model Checking Software, (155-171)
- Ruys T and Kars P Gossiping girls are all alike Proceedings of the 19th international conference on Model Checking Software, (117-136)
- André É, Choppy C and Klai K (2012). Formalizing non-concurrent UML state machines using colored petri nets, ACM SIGSOFT Software Engineering Notes, 37:4, (1-8), Online publication date: 16-Jul-2012.
- Yatake K and Aoki T (2012). SMT-based enumeration of object graphs from UML class diagrams, ACM SIGSOFT Software Engineering Notes, 37:4, (1-8), Online publication date: 16-Jul-2012.
- Groce A and Erwig M Finding common ground: choose, assert, and assume Proceedings of the Ninth International Workshop on Dynamic Analysis, (12-17)
- Lal A, Qadeer S and Lahiri S A solver for reachability modulo theories Proceedings of the 24th international conference on Computer Aided Verification, (427-443)
- Esparza J, Gaiser A and Kiefer S Proving termination of probabilistic programs using patterns Proceedings of the 24th international conference on Computer Aided Verification, (123-138)
- Shan Z and Kumar A (2012). Optimal Adapter Creation for Process Composition in Synchronous vs. Asynchronous Communication, ACM Transactions on Management Information Systems, 3:2, (1-33), Online publication date: 1-Jul-2012.
- Alzahrani M and Georgieva L Modelling trusted web applications Proceedings of the 6th KES international conference on Agent and Multi-Agent Systems: technologies and applications, (524-533)
- Blašković B, Skočir Z and Humski L Scenario modeling and verification for business processes Proceedings of the 6th KES international conference on Agent and Multi-Agent Systems: technologies and applications, (414-423)
- Faria J, Martins J and Pinto J An approach to model checking ada programs Proceedings of the 17th Ada-Europe international conference on Reliable Software Technologies, (105-118)
- Deng D, Zhang W, Wang B, Zhao P and Lu S Understanding the interleaving-space overlap across inputs and software versions Proceedings of the 4th USENIX conference on Hot Topics in Parallelism, (17-17)
- Cordy M, Classen A, Perrouin G, Schobbens P, Heymans P and Legay A Simulation-based abstractions for software product-line model checking Proceedings of the 34th International Conference on Software Engineering, (672-682)
- Rodrigues Vieira E, Vieira D and Gallois J (2012). Challenges of a Validation Process Based on Models: An Industrial Case Study, Bell Labs Technical Journal, 17:1, (229-246), Online publication date: 1-Jun-2012.
- Alvaro P, Hutchinson A, Conway N, Marczak W and Hellerstein J BloomUnit Proceedings of the Fifth International Workshop on Testing Database Systems, (1-7)
- Kim M, Kim Y and Choi Y (2011). Concolic testing of the multi-sector read operation for flash storage platform software, Formal Aspects of Computing, 24:3, (355-374), Online publication date: 1-May-2012.
- Mühlberg J and Lüttgen G (2011). Verifying compiled file system code, Formal Aspects of Computing, 24:3, (375-391), Online publication date: 1-May-2012.
- Canini M, Venzano D, Perešíni P, Kostić D and Rexford J A NICE way to test openflow applications Proceedings of the 9th USENIX conference on Networked Systems Design and Implementation, (10-10)
- Zave P (2012). Using lightweight modeling to understand chord, ACM SIGCOMM Computer Communication Review, 42:2, (49-57), Online publication date: 29-Mar-2012.
- Bae K and Meseguer J Model checking LTLR formulas under localized fairness Proceedings of the 9th international conference on Rewriting Logic and Its Applications, (99-117)
- Jain S, Zhang C and Scholz B Translating flowcharts to non-deterministic languages Proceedings of the ACM SIGPLAN 2012 workshop on Partial evaluation and program manipulation, (155-162)
- Hallé S, Villemaire R, Cherkaoui O and Deca R A logical approach to data-aware automated sequence generation Transactions on Computational Science XV, (192-216)
- Morse J, Cordeiro L, Nicole D and Fischer B Context-bounded model checking of LTL properties for ANSI-C software Proceedings of the 9th international conference on Software engineering and formal methods, (302-317)
- Vassev E and Hinchey M Developing model-checking mechanisms for ASSL Proceedings of the 9th international conference on Software engineering and formal methods, (19-34)
- Groce A Coverage rewarded Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering, (380-383)
- Eian M and Mjølsnes S The modeling and comparison of wireless network denial of service attacks Proceedings of the 3rd ACM SOSP Workshop on Networking, Systems, and Applications on Mobile Handhelds, (1-6)
- Partridge C (2011). Forty data communications research questions, ACM SIGCOMM Computer Communication Review, 41:5, (24-35), Online publication date: 22-Oct-2011.
- Brosch P, Egly U, Gabmeyer S, Kappel G, Seidl M, Tompits H, Widl M and Wimmer M Towards semantics-aware merge support in optimistic model versioning Proceedings of the 2011th international conference on Models in Software Engineering, (246-256)
- Cheng C, Bensalem S, Chen Y, Yan R, Jobstmann B, Ruess H, Buckl C and Knoll A Algorithms for synthesizing priorities in component-based systems Proceedings of the 9th international conference on Automated technology for verification and analysis, (150-167)
- Harel D, Lampert R, Marron A and Weiss G Model-checking behavioral programs Proceedings of the ninth ACM international conference on Embedded software, (279-288)
- Havelund K and Holzmann G Software certification Proceedings of the ninth ACM international conference on Embedded software, (205-210)
- Bentea L and Owe O A probabilistic framework for object-oriented modeling and analysis of distributed systems Proceedings of the 2011 international conference on Formal Verification of Object-Oriented Software, (105-122)
- Buchs D, Hostettler S and Marechal A Experience-based model refinement Proceedings of the Third international conference on Software engineering for resilient systems, (40-47)
- André É and Soulat R Synthesis of timing parameters satisfying safety properties Proceedings of the 5th international conference on Reachability problems, (31-44)
- Homoceanu G and Huhn M Tool support for agent-based systems in ptolemy Proceedings of the International Workshop on Security and Dependability for Resource Constrained Embedded Systemss, (1-6)
- Webster M, Fisher M, Cameron N and Jump M Formal methods for the certification of autonomous unmanned aircraft systems Proceedings of the 30th international conference on Computer safety, reliability, and security, (228-242)
- Bonichon R, Canet G, Correnson L, Goubault E, Haucourt E, Hirschowitz M, Labbé S and Mimram S Rigorous evidence of freedom from concurrency faults in industrial control software Proceedings of the 30th international conference on Computer safety, reliability, and security, (85-98)
- Jörges S, Margaria T and Steffen B (2011). Assuring property conformance of code generators via model checking, Formal Aspects of Computing, 23:5, (589-606), Online publication date: 1-Sep-2011.
- Fares E, Bodeveix J and Filali M Design of a BPEL verification tool Proceedings of the 8th international conference on Web Services and Formal Methods, (95-110)
- Lomuscio A, Penczek W, Solanki M and Szreter M (2011). Runtime Monitoring of Contract Regulated Web Services, Fundamenta Informaticae, 111:3, (339-355), Online publication date: 1-Aug-2011.
- Krepska E, Kielmann T, Fokkink W and Bal H (2011). HipG, ACM SIGOPS Operating Systems Review, 45:2, (3-13), Online publication date: 18-Jul-2011.
- Yasmeen A and Gunter E Automated framework for formal operator task analysis Proceedings of the 2011 International Symposium on Software Testing and Analysis, (78-88)
- De Vos B, Kats L and Pronk C EpiSpin Proceedings of the 18th international SPIN conference on Model checking software, (177-182)
- Linden A and Wolper P A verification-based approach to memory fence insertion in relaxed memory systems Proceedings of the 18th international SPIN conference on Model checking software, (144-160)
- Mali Y and Van Wyk E Building extensible specifications and implementations of Promela with AbleP Proceedings of the 18th international SPIN conference on Model checking software, (108-125)
- Černý P, Chatterjee K, Henzinger T, Radhakrishna A and Singh R Quantitative synthesis for concurrent programs Proceedings of the 23rd international conference on Computer aided verification, (243-259)
- Bae K and Meseguer J State/event-based LTL model checking under parametric generalized fairness Proceedings of the 23rd international conference on Computer aided verification, (132-148)
- Schwartz-Narbonne D, Liu F, Pondicherry T, August D and Malik S Parallel assertions for debugging parallel programs Proceedings of the Ninth ACM/IEEE International Conference on Formal Methods and Models for Codesign, (181-190)
- Bensalem S, Griesmayer A, Legay A, Nguyen T and Peled D Efficient deadlock detection for concurrent systems Proceedings of the Ninth ACM/IEEE International Conference on Formal Methods and Models for Codesign, (119-129)
- Gaudel M Checking models, proving programs, and testing systems Proceedings of the 5th international conference on Tests and proofs, (1-13)
- Costa G and Matteucci I Elective temporal logic Proceedings of the joint ACM SIGSOFT conference -- QoSA and ACM SIGSOFT symposium -- ISARCS on Quality of software architectures -- QoSA and architecting critical systems -- ISARCS, (143-152)
- Slåtten V and Herrmann P Contracts for multi-instance UML activities Proceedings of the joint 13th IFIP WG 6.1 and 30th IFIP WG 6.1 international conference on Formal techniques for distributed systems, (304-318)
- Atkinson K, Bench-Capon T, Cartwright D and Wyner A Semantic models for policy deliberation Proceedings of the 13th International Conference on Artificial Intelligence and Law, (81-90)
- Cassou D, Balland E, Consel C and Lawall J Leveraging software architectures to guide and verify the development of sense/compute/control applications Proceedings of the 33rd International Conference on Software Engineering, (431-440)
- Holzmann G and Florian M (2011). Model checking with bounded context switching, Formal Aspects of Computing, 23:3, (365-389), Online publication date: 1-May-2011.
- Groote J, Kouters T and Osaiweran A Specification guidelines to avoid the state space explosion problem Proceedings of the 4th IPM international conference on Fundamentals of Software Engineering, (112-127)
- Kumazawa T and Tamai T Counter example-based error localization of behavior models Proceedings of the Third international conference on NASA Formal methods, (222-236)
- Berendsen J, Gebremichael B, Vaandrager F and Zhang M (2011). Formal specification and analysis of zeroconf using uppaalS, ACM Transactions on Embedded Computing Systems, 10:3, (1-32), Online publication date: 1-Apr-2011.
- Heckman S and Williams L (2011). A systematic literature review of actionable alert identification techniques for automated static code analysis, Information and Software Technology, 53:4, (363-387), Online publication date: 1-Apr-2011.
- Garavel H, Lang F, Mateescu R and Serwe W CADP 2010 Proceedings of the 17th international conference on Tools and algorithms for the construction and analysis of systems: part of the joint European conferences on theory and practice of software, (372-387)
- Tsay Y, Tsai M, Chang J and Chang Y Büchi store Proceedings of the 17th international conference on Tools and algorithms for the construction and analysis of systems: part of the joint European conferences on theory and practice of software, (262-266)
- Holzmann G Reliable software development Proceedings of the 17th international conference on Tools and algorithms for the construction and analysis of systems: part of the joint European conferences on theory and practice of software, (1-2)
- Gabbay M and Ciancia V Freshness and name-restriction in sets of traces with names Proceedings of the 14th international conference on Foundations of software science and computational structures: part of the joint European conferences on theory and practice of software, (365-380)
- Chang L and He X A model transformation approach for verifying multi-agent systems using SPIN Proceedings of the 2011 ACM Symposium on Applied Computing, (37-42)
- Sridhar M and Hamlen K Flexible in-lined reference monitor certification Proceedings of the 5th ACM workshop on Programming languages meets program verification, (55-60)
- Cook B, Fisher J, Krepska E and Piterman N Proving stabilization of biological systems Proceedings of the 12th international conference on Verification, model checking, and abstract interpretation, (134-149)
- Hojjat H, Mousavi M and Sirjani M (2011). Formal Analysis of SystemC Designs in Process Algebra, Fundamenta Informaticae, 107:1, (19-42), Online publication date: 1-Jan-2011.
- Salamah S, Gates A, Roach S and Engskow M (2011). Towards support for software model checking, Advances in Software Engineering, 2011, (1-13), Online publication date: 1-Jan-2011.
- Frappier M, Fraikin B, Chossart R, Chane-Yack-Fa R and Ouenzar M Comparison of model checking tools for information systems Proceedings of the 12th international conference on Formal engineering methods and software engineering, (581-596)
- Akhtar S, Merz S and Quinson M A high-level language for modeling algorithms and their properties Proceedings of the 13th Brazilian conference on Formal methods: foundations and applications, (49-63)
- Leuschel M and Bendisposto J Directed model checking for B Proceedings of the 13th Brazilian conference on Formal methods: foundations and applications, (1-16)
- Ulrich A, Alikacem E, Hallal H and Boroday S From scenarios to test implementations via Promela Proceedings of the 22nd IFIP WG 6.1 international conference on Testing software and systems, (236-249)
- Balland E and Consel C Open platforms Programming Support Innovations for Emerging Distributed Applications, (1-4)
- Goldsby H and Cheng B Automatically discovering properties that specify the latent behavior of UML models Proceedings of the 13th international conference on Model driven engineering languages and systems: Part I, (316-330)
- Donaldson R, Talcott C, Knapp M and Calder M Understanding signalling networks as collections of signal transduction pathways Proceedings of the 8th International Conference on Computational Methods in Systems Biology, (86-95)
- Chen Z and Motet G Nevertrace claims for model checking Proceedings of the 17th international SPIN conference on Model checking software, (162-179)
- Ehlers R and Finkbeiner B On the virtue of patience Proceedings of the 17th international SPIN conference on Model checking software, (129-145)
- de Jonge M and Ruys T The SpinJa model checker Proceedings of the 17th international SPIN conference on Model checking software, (124-128)
- Edelkamp S and Sulewski D Efficient explicit-state model checking on general purpose graphics processors Proceedings of the 17th international SPIN conference on Model checking software, (106-123)
- Merino P and Salmerón A Combining SPIN with ns-2 for protocol Optimization Proceedings of the 17th international SPIN conference on Model checking software, (40-57)
- Soupionis Y, Basagiannis S, Katsaros P and Gritzalis D A formally verified mechanism for countering SPIT Proceedings of the 5th international conference on Critical Information Infrastructures Security, (128-139)
- Liu Y, Sun J and Dong J Developing model checkers using PAT Proceedings of the 8th international conference on Automated technology for verification and analysis, (371-377)
- Chatzigiannakis I, Michail O and Spirakis P Algorithmic verification of population protocols Proceedings of the 12th international conference on Stabilization, safety, and security of distributed systems, (221-235)
- van Amstel M, van den Brand M and Engelen L An exercise in iterative domain-specific language design Proceedings of the Joint ERCIM Workshop on Software Evolution (EVOL) and International Workshop on Principles of Software Evolution (IWPSE), (48-57)
- Hallé S Automated generation of web service stubs using LTL satisfiability solving Proceedings of the 7th international conference on Web services and formal methods, (42-55)
- Malkis A, Podelski A and Rybalchenko A Thread-modular counterexample-guided abstraction refinement Proceedings of the 17th international conference on Static analysis, (356-372)
- Zeng R and He X Analyzing a formal specification of Mondex using model checking Proceedings of the 7th International colloquium conference on Theoretical aspects of computing, (214-229)
- André É and Fribourg L Behavioral cartography of timed automata Proceedings of the 4th international conference on Reachability problems, (76-90)
- Claßen J and Lakemeyer G On the Verification of Very Expressive Temporal Properties of Non-terminating Golog Programs Proceedings of the 2010 conference on ECAI 2010: 19th European Conference on Artificial Intelligence, (887-892)
- Bond G, Smith T, Cheung E and Zave P Specification and evaluation of transparent behavior for SIP back-to-back user agents Principles, Systems and Applications of IP Telecommunications, (48-58)
- Yang C and Duan Z Compositional verification with stutter-invariant propositional projection temporal logic Proceedings of the 14th WSEAS international conference on Computers: part of the 14th WSEAS CSCC multiconference - Volume I, (272-280)
- Hahn E, Hermanns H, Wachter B and Zhang L PARAM Proceedings of the 22nd international conference on Computer Aided Verification, (660-664)
- Černý P, Radhakrishna A, Zufferey D, Chaudhuri S and Alur R Model checking of linearizability of concurrent list implementations Proceedings of the 22nd international conference on Computer Aided Verification, (465-479)
- Pnueli A, Sa'ar Y and Zuck L JTLV Proceedings of the 22nd international conference on Computer Aided Verification, (171-174)
- Edelkamp S, Kellershoff M and Sulewski D Program model checking via action planning Proceedings of the 6th international conference on Model checking and artificial intelligence, (32-51)
- Edelkamp S and Sulewski D External memory breadth-first search with delayed duplicate detection on the GPU Proceedings of the 6th international conference on Model checking and artificial intelligence, (12-31)
- Weber I, Hoffmann J and Mendling J (2010). Beyond soundness, Distributed and Parallel Databases, 27:3, (271-343), Online publication date: 1-Jun-2010.
- Rungta N and Mercer E Slicing and dicing bugs in concurrent programs Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - Volume 2, (195-198)
- Kobayashi N and Sangiorgi D (2008). A hybrid type system for lock-freedom of mobile processes, ACM Transactions on Programming Languages and Systems, 32:5, (1-49), Online publication date: 1-May-2010.
- Brandt J, Schneider K and Shukla S (2010). Translating concurrent action oriented specifications to synchronous guarded actions, ACM SIGPLAN Notices, 45:4, (47-56), Online publication date: 13-Apr-2010.
- Brandt J, Schneider K and Shukla S Translating concurrent action oriented specifications to synchronous guarded actions Proceedings of the ACM SIGPLAN/SIGBED 2010 conference on Languages, compilers, and tools for embedded systems, (47-56)
- Vassev E and Hinchey M Software verification of autonomic systems developed with ASSL Proceedings of the 16th Monterey conference on Foundations of computer software: modeling, development, and verification of adaptive systems, (1-16)
- Hurnaus D and Prähofer H Programming assistance based on contracts and modular verification in the automation domain Proceedings of the 2010 ACM Symposium on Applied Computing, (2544-2551)
- Ben-Ari M (2010). A primer on model checking, ACM Inroads, 1:1, (40-47), Online publication date: 1-Mar-2010.
- Aminof B, Kupferman O and Lampert R (2010). Reasoning about online algorithms with weighted automata, ACM Transactions on Algorithms, 6:2, (1-36), Online publication date: 1-Mar-2010.
- Lin C, Wolf M, Koutsoukos X, Neema S and Sztipanovits J (2010). System and software architectures of distributed smart cameras, ACM Transactions on Embedded Computing Systems, 9:4, (1-30), Online publication date: 1-Mar-2010.
- Kong W, Shiraishi T, Mizushima Y, Katahira N, Fukuda A and Watanabe M Formal analysis of STM design with SAL infinite bounded model checker Proceedings of the 12th international conference on Advanced communication technology, (1003-1008)
- Furia C, Mandrioli D, Morzenti A and Rossi M (2010). Modeling time in computing, ACM Computing Surveys, 42:2, (1-59), Online publication date: 1-Feb-2010.
- Miller S, Whalen M and Cofer D (2010). Software model checking takes off, Communications of the ACM, 53:2, (58-64), Online publication date: 1-Feb-2010.
- Kloetzer M and Belta C (2010). Automatic deployment of distributed teams of robots from temporal logic motion specifications, IEEE Transactions on Robotics, 26:1, (48-61), Online publication date: 1-Feb-2010.
- Harrison M and Massink M (2010). Modelling Interactive Experience, Function and Performance in Ubiquitous Systems, Electronic Notes in Theoretical Computer Science (ENTCS), 261, (23-42), Online publication date: 1-Feb-2010.
- Lahiri S, Malkis A and Qadeer S Abstract threads Proceedings of the 11th international conference on Verification, Model Checking, and Abstract Interpretation, (231-246)
- Hölzl M, Knapp A and Zhang G Modeling the car crash crisis management system using HiLA Transactions on aspect-oriented software development VII, (234-271)
- Rensink A The edge of graph transformation Graph transformations and model-driven engineering, (6-32)
- Hölzl M, Knapp A and Zhang G Modeling the car crash crisis management system using HiLA Transactions on aspect-oriented software development VII, (234-271)
- Montali M, Pesic M, Aalst W, Chesani F, Mello P and Storari S (2010). Declarative specification and verification of service choreographiess, ACM Transactions on the Web, 4:1, (1-62), Online publication date: 1-Jan-2010.
- Abdulsalam A Using model checking tool for teaching concurrent programming concepts Proceedings of the 6th international conference on Innovations in information technology, (146-150)
- Dos Santos O, Woodcock J, Paige R and King S The use of model transformation in the INESS project Proceedings of the 8th international conference on Formal methods for components and objects, (147-165)
- Hoang T, Kuruma H, Basin D and Abrial J (2009). Developing topology discovery in Event-B, Science of Computer Programming, 74:11-12, (879-899), Online publication date: 1-Nov-2009.
- Ding J, Clarke P, Argote-Garcia G and He X (2009). A methodology for evaluating test coverage criteria of high levelPetri nets, Information and Software Technology, 51:11, (1520-1533), Online publication date: 1-Nov-2009.
- Chen J and Huang L Formal verification of service composition in pervasive computing environments Proceedings of the First Asia-Pacific Symposium on Internetware, (1-5)
- Geldenhuys J, Hansen H and Valmari A Exploring the Scope for Partial Order Reduction Automated Technology for Verification and Analysis, (39-53)
- Woodcock J, Larsen P, Bicarregui J and Fitzgerald J (2009). Formal methods, ACM Computing Surveys, 41:4, (1-36), Online publication date: 1-Oct-2009.
- Zhou L (2009). Building reliable large-scale distributed systems, ACM SIGACT News, 40:3, (78-85), Online publication date: 25-Sep-2009.
- Jing L and Jinhua L Model checking the SET purchasing process protocol with SPIN Proceedings of the 5th International Conference on Wireless communications, networking and mobile computing, (4486-4489)
- Kumar R and Mercer E (2009). Verifying Communication Protocols Using Live Sequence Chart Specifications, Electronic Notes in Theoretical Computer Science (ENTCS), 250:2, (33-48), Online publication date: 1-Sep-2009.
- Donaldson A (2009). Vector Symmetry Reduction, Electronic Notes in Theoretical Computer Science (ENTCS), 250:2, (3-18), Online publication date: 1-Sep-2009.
- James M, Shapiro A, Springer P and Zima H (2009). Adaptive Fault Tolerance for Scalable Cluster Computing in Space, International Journal of High Performance Computing Applications, 23:3, (227-241), Online publication date: 1-Aug-2009.
- Martínez E, Díaz G, Martínez C, Cambronero M and Valero V Time Ordering Architecture in SCA Proceedings of the 2009 conference on Techniques and Applications for Mobile Commerce: Proceedings of TAMoCo 2009, (117-126)
- Groce A (Quickly) testing the tester via path coverage Proceedings of the Seventh International Workshop on Dynamic Analysis, (22-28)
- Rungta N and Mercer E Clash of the Titans Proceedings of the 7th Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging, (1-10)
- Stengel Z and Bultan T Analyzing singularity channel contracts Proceedings of the eighteenth international symposium on Software testing and analysis, (13-24)
- Bottrighi A, Chesani F, Mello P, Montali M, Montani S, Storari S and Terenziani P Analysis of the GLARE and GPROVE approaches to clinical guidelines Proceedings of the 2009 AIME international conference on Knowledge Representation for Health-Care: data, Processes and Guidelines, (76-87)
- Kuliamin V (2009). Integration of verification methods for program systems, Programming and Computing Software, 35:4, (212-222), Online publication date: 1-Jul-2009.
- Armoni M and Ben-Ari M (2009). The concept of nondeterminism, ACM SIGCSE Bulletin, 41:2, (141-160), Online publication date: 25-Jun-2009.
- Nishihara H, Shinozaki K, Hayamizu K, Aoki T, Taguchi K and Kumeno F (2009). Model checking education for software engineers in Japan, ACM SIGCSE Bulletin, 41:2, (45-50), Online publication date: 25-Jun-2009.
- Tahara Y, Yoshioka N, Taguchi K, Aoki T and Honiden S (2009). Evolution of a course on model checking for practical applications, ACM SIGCSE Bulletin, 41:2, (38-44), Online publication date: 25-Jun-2009.
- Vree A, Vlaovič B and Brezočnik Z (2009). Sdl2pml - Tool for automated generation of Promela model from SDL specification, Computer Standards & Interfaces, 31:4, (779-786), Online publication date: 1-Jun-2009.
- Lomuscio A and Solanki M Towards an Agent Based Approach for Verification of OWL-S Process Models Proceedings of the 6th European Semantic Web Conference on The Semantic Web: Research and Applications, (578-592)
- Matousek T and Jezek P (2009). DeSpec, Electronic Notes in Theoretical Computer Science (ENTCS), 203:7, (55-69), Online publication date: 1-Apr-2009.
- Gallardo M, Merino P and Sanán D (2009). Model Checking Dynamic Memory Allocation in Operating Systems, Journal of Automated Reasoning, 42:2-4, (229-264), Online publication date: 1-Apr-2009.
- Timm I and Schumann R Performance measurement of multiagent systems Proceedings of the 2009 Spring Simulation Multiconference, (1-8)
- Hierons R, Bogdanov K, Bowen J, Cleaveland R, Derrick J, Dick J, Gheorghe M, Harman M, Kapoor K, Krause P, Lüttgen G, Simons A, Vilkomir S, Woodward M and Zedan H (2009). Using formal specifications to support testing, ACM Computing Surveys, 41:2, (1-76), Online publication date: 1-Feb-2009.
- Rungta N and Mercer E Guided model checking for programs with polymorphism Proceedings of the 2009 ACM SIGPLAN workshop on Partial evaluation and program manipulation, (21-30)
- Samset H and Bræk R Dealing with Active and Stateful Services in the Service-Oriented Architecture Service-Oriented Computing - ICSOC 2007 Workshops, (268-281)
- Aminof B, Kupferman O and Lampert R Reasoning about online algorithms with weighted automata Proceedings of the twentieth annual ACM-SIAM symposium on Discrete algorithms, (835-844)
- Niewiadomski A, Penczek W and Szreter M (2009). A New Approach to Model Checking of UML State Machines, Fundamenta Informaticae, 93:1-3, (289-303), Online publication date: 1-Jan-2009.
- Niewiadomski A, Penczek W and Szreter M (2009). A New Approach to Model Checking of UML State Machines, Fundamenta Informaticae, 93:1-3, (289-303), Online publication date: 1-Jan-2009.
- Pu G, Zhao Y, Wang Z, Feng L, Zhu H and He J A Denotational Model for Web Services Choreography Proceedings of the 5th International Conference on Distributed Computing and Internet Technology, (1-12)
- Holzmann G, Joshi R and Groce A (2008). Model driven code checking, Automated Software Engineering, 15:3-4, (283-297), Online publication date: 1-Dec-2008.
- Hartel P, Ruys T and Geilen M Scheduling optimisations for SPIN to minimise buffer requirements in synchronous data flow Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, (1-10)
- Sinha N Symbolic program analysis using term rewriting and generalization Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, (1-9)
- Donaldson A and Miller A (2008). Automatic Symmetry Detection for Promela, Journal of Automated Reasoning, 41:3-4, (251-293), Online publication date: 1-Nov-2008.
- Cheung E and Zave P Generalized Third-Party Call Control in SIP Networks Principles, Systems and Applications of IP Telecommunications. Services and Security for Next Generation Networks, (45-68)
- Zave P Understanding SIP through Model-Checking Principles, Systems and Applications of IP Telecommunications. Services and Security for Next Generation Networks, (256-279)
- Ratkowski A and Zalewski A Transformational design of business processes for SOA Proceedings of the Third IFIP TC 2 Central and East European conference on Software engineering techniques, (76-90)
- Hamberg R and Vaandrager F (2008). Using model checkers in an introductory course on operating systems, ACM SIGOPS Operating Systems Review, 42:6, (101-111), Online publication date: 1-Oct-2008.
- Claßen J and Lakemeyer G A logic for non-terminating Golog programs Proceedings of the Eleventh International Conference on Principles of Knowledge Representation and Reasoning, (589-599)
- Holzmann G, Joshi R and Groce A Swarm Verification Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering, (1-6)
- Walkinshaw N and Bogdanov K Inferring Finite-State Models with Temporal Constraints Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering, (248-257)
- Bordini R, Dennis L, Farwer B and Fisher M Automated Verification of Multi-Agent Programs Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering, (69-78)
- Furia C and Spoletini P Tomorrow and All our Yesterdays Proceedings of the 5th international colloquium on Theoretical Aspects of Computing, (126-140)
- Blom S and Pol J Symbolic Reachability for Process Algebras with Recursive Data Types Proceedings of the 5th international colloquium on Theoretical Aspects of Computing, (81-95)
- O'Leary J, Saha B and Tuttle M Model checking transactional memory with spin Proceedings of the twenty-seventh ACM symposium on Principles of distributed computing, (424-424)
- Ciesinski F, Baier C, Größer M and Parker D Generating Compact MTBDD-Representations from Probmela Specifications Proceedings of the 15th international workshop on Model Checking Software, (60-76)
- Zaks A and Joshi R Verifying Multi-threaded C Programs with SPIN Proceedings of the 15th international workshop on Model Checking Software, (325-342)
- Yang Y, Chen X, Gopalakrishnan G and Kirby R Efficient Stateful Dynamic Partial Order Reduction Proceedings of the 15th international workshop on Model Checking Software, (288-305)
- Nguyen V and Ruys T Incremental Hashing for Spin Proceedings of the 15th international workshop on Model Checking Software, (232-249)
- Leue S, Ştefănescu A and Wei W Dependency Analysis for Control Flow Cycles in Reactive Communicating Processes Proceedings of the 15th international workshop on Model Checking Software, (176-195)
- Groce A and Joshi R Random testing and model checking Proceedings of the 2008 international workshop on dynamic analysis: held in conjunction with the ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2008), (22-28)
- Pǎsǎreanu C, Mehlitz P, Bushnell D, Gundy-Burlet K, Lowry M, Person S and Pape M Combining unit-level symbolic execution and system-level concrete execution for testing nasa software Proceedings of the 2008 international symposium on Software testing and analysis, (15-26)
- Ramanathan M, Sen K, Grama A and Jagannathan S Protocol Inference Using Static Path Profiles Proceedings of the 15th international symposium on Static Analysis, (78-92)
- Goldsby H and Cheng B Avida-MDE Proceedings of the 10th annual conference on Genetic and evolutionary computation, (1751-1758)
- Brummayer R, Biere A and Lonsing F BTOR Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning, (33-38)
- Vakkalanka S, Gopalakrishnan G and Kirby R Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings Proceedings of the 20th international conference on Computer Aided Verification, (66-79)
- Havelund K Runtime Verification of C Programs Proceedings of the 20th IFIP TC 6/WG 6.1 international conference on Testing of Software and Communicating Systems: 8th International Workshop, (7-22)
- Massacci F and Siahaan I Simulating midlet's security claims with automata modulo theory Proceedings of the third ACM SIGPLAN workshop on Programming languages and analysis for security, (1-9)
- Koskinen E and Herlihy M Dreadlocks Proceedings of the twentieth annual symposium on Parallelism in algorithms and architectures, (297-303)
- Long B, Dingel J and Graham T Experience applying the SPIN model checker to an industrial telecommunications system Proceedings of the 30th international conference on Software engineering, (693-702)
- Adamek J and Hnetynka P Perspectives in component-based software engineering Proceedings of the 2008 international workshop on Software Engineering in east and south europe, (35-42)
- Tadjouddine E, Guerin F and Vasconcelos W Abstractions for model-checking game-theoretic properties of auctions Proceedings of the 7th international joint conference on Autonomous agents and multiagent systems - Volume 3, (1613-1616)
- Dennis L, Farwer B, Bordini R and Fisher M A flexible framework for verifying agent programs Proceedings of the 7th international joint conference on Autonomous agents and multiagent systems - Volume 3, (1303-1306)
- Günay A and Yolum P Semantic matchmaking of web services using model checking Proceedings of the 7th international joint conference on Autonomous agents and multiagent systems - Volume 1, (273-280)
- Ding J, Argote-Garcia G, Clarke P and He X Evaluating test adequacy coverage of high level petri nets using spin Proceedings of the 3rd international workshop on Automation of software test, (71-78)
- Lowe G (2008). Specification of communicating processes: temporal logic versus refusals-based refinement, Formal Aspects of Computing, 20:3, (277-294), Online publication date: 1-May-2008.
- Chen X, Huang G and Mei H Towards automatic verification of web-based SOA applications Proceedings of the 10th Asia-Pacific web conference on Progress in WWW research and development, (528-536)
- Demirbas M, Soysal O and Hussain M TRANSACT Proceedings of the 7th international conference on Information processing in sensor networks, (295-306)
- Claessen K and Svensson H Finding counter examples in induction proofs Proceedings of the 2nd international conference on Tests and proofs, (48-65)
- Yu X, Wang Z, Pu G, Mao D and Liu J (2008). The Verification of rCOS Using Spin, Electronic Notes in Theoretical Computer Science (ENTCS), 207, (49-67), Online publication date: 1-Apr-2008.
- Finkbeiner B, Peter H and Schewe S RESY Proceedings of the Theory and practice of software, 14th international conference on Tools and algorithms for the construction and analysis of systems, (463-466)
- Tsay Y, Chen Y, Tsai M, Chan W and Luo C GOAL extended Proceedings of the Theory and practice of software, 14th international conference on Tools and algorithms for the construction and analysis of systems, (346-350)
- Edelkamp S, Jabbar S and Sulewski D (2008). Distributed Verification of Multi-threaded C++ Programs, Electronic Notes in Theoretical Computer Science (ENTCS), 198:1, (33-46), Online publication date: 1-Feb-2008.
- Holzmann G (2008). A Stack-Slicing Algorithm for Multi-Core Model Checking, Electronic Notes in Theoretical Computer Science (ENTCS), 198:1, (3-16), Online publication date: 1-Feb-2008.
- Groce A and Joshi R Extending model checking with dynamic analysis Proceedings of the 9th international conference on Verification, model checking, and abstract interpretation, (142-156)
- Zhang Y and Ding Y (2008). CTL model update for system modifications, Journal of Artificial Intelligence Research, 31:1, (113-155), Online publication date: 1-Jan-2008.
- Chirichiello A and Salaün G (2007). Encoding process algebraic descriptions of web services into BPEL, Web Intelligence and Agent Systems, 5:4, (419-434), Online publication date: 1-Dec-2007.
- Casella G and Mascardi V (2007). West2East: exploiting WEb Service Technologies to Engineer Agent-based SofTware, International Journal of Agent-Oriented Software Engineering, 1:3/4, (396-434), Online publication date: 1-Dec-2007.
- Yamada C and Nagata Y An efficient specification for model checking using check-points extraction method Proceedings of the 7th Conference on 7th WSEAS International Conference on Applied Computer Science - Volume 7, (208-213)
- Krüger I, Farcas C, Farcas E and Menarini M Requirements modeling for embedded realtime systems Proceedings of the 2007 International Dagstuhl conference on Model-based engineering of embedded real-time systems, (155-199)
- Noll T and Schlich B Delayed nondeterminism in model checking embedded systems assembly code Proceedings of the 3rd international Haifa verification conference on Hardware and software: verification and testing, (185-201)
- Noll T and Schlich B Delayed Nondeterminism in Model Checking Embedded Systems Assembly Code Hardware and Software: Verification and Testing, (185-201)
- Salamah S, Gates A, Kreinovich V and Roach S Using patterns and composite propositions to automate the generation of LTL specifications Proceedings of the 5th international conference on Automated technology for verification and analysis, (533-542)
- Bošnački D, Donaldson A, Leuschel M and Massart T Efficient approximate verification of Promela models via symmetry markers Proceedings of the 5th international conference on Automated technology for verification and analysis, (300-315)
- Saha I, Misra J and Roy S Timeout and calendar based finite state modeling and verification of real-time systems Proceedings of the 5th international conference on Automated technology for verification and analysis, (284-299)
- Dax C, Eisinger J and Klaedtke F Mechanizing the powerset construction for restricted classes of ω-automata Proceedings of the 5th international conference on Automated technology for verification and analysis, (223-236)
- Pace G, Prisacariu C and Schneider G Model checking contracts Proceedings of the 5th international conference on Automated technology for verification and analysis, (82-97)
- Pace G, Prisacariu C and Schneider G Model Checking Contracts – A Case Study Automated Technology for Verification and Analysis, (82-97)
- Salamah S, Gates A, Kreinovich V and Roach S Using Patterns and Composite Propositions to Automate the Generation of LTL Specifications Automated Technology for Verification and Analysis, (533-542)
- Kim M Formal Modeling and Verification of High-Availability Protocol for Network Security Appliances Automated Technology for Verification and Analysis, (489-500)
- Saha I, Misra J and Roy S Timeout and Calendar Based Finite State Modeling and Verification of Real-Time Systems Automated Technology for Verification and Analysis, (284-299)
- Dax C, Eisinger J and Klaedtke F Mechanizing the Powerset Construction for Restricted Classes of ω-Automata Automated Technology for Verification and Analysis, (223-236)
- Bakhshi R, Bonnet F, Fokkink W and Haverkort B (2007). Formal analysis techniques for gossiping protocols, ACM SIGOPS Operating Systems Review, 41:5, (28-36), Online publication date: 1-Oct-2007.
- Holzmann G and Bosnacki D (2007). The Design of a Multicore Extension of the SPIN Model Checker, IEEE Transactions on Software Engineering, 33:10, (659-674), Online publication date: 1-Oct-2007.
- Konrad S, Goldsby H and Cheng B i2MAP Proceedings of the 10th international conference on Model Driven Engineering Languages and Systems, (451-466)
- Hallé S, Villemaire R, Cherkaoui O, Tremblay J and Ghandour B Extending model checking to data-aware temporal properties of web services Proceedings of the 4th international conference on Web services and formal methods, (31-45)
- Matta A, Rossi M, Spoletini P, Mandrioli D, Semeraro Q and Tolio T FM for FMS Proceedings of the 4th international conference on Theoretical aspects of computing, (366-380)
- Sankaranarayanan S, Chang R, Jiang G and Ivančić F State space exploration using feedback constraint generation and Monte-Carlo sampling Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, (321-330)
- Loyauté G, Forax R and Roussel G A Java toolkit for the design and the automatic checking of server architectures Proceedings of the 5th international symposium on Principles and practice of programming in Java, (113-122)
- Viganò F and Colombetti M Symbolic model checking of institutions Proceedings of the ninth international conference on Electronic commerce, (35-44)
- Man K, Fedeli A, Mercaldi M, Boubekeur M and Schellekens M SC2SCFL Proceedings of the 7th international conference on Embedded computer systems: architectures, modeling, and simulation, (34-45)
- Brambilla M, Cabot J and Moreno N Tool support for model checking of web application designs Proceedings of the 7th international conference on Web engineering, (533-538)
- Muccini H, Polini A, Ricci F and Bertolino A Monitoring architectural properties in dynamic component-based systems Proceedings of the 10th international conference on Component-based software engineering, (124-139)
- Toben T Non-interference properties for data-type reduction of communicating systems Proceedings of the 6th international conference on Integrated formal methods, (619-638)
- Pelánek R Model classifications and automated verification Proceedings of the 12th international conference on Formal methods for industrial critical systems, (149-163)
- Pelánek R BEEM Proceedings of the 14th international SPIN conference on Model checking software, (263-267)
- Lafuente A Towards model checking spatial properties with SPIN Proceedings of the 14th international SPIN conference on Model checking software, (223-242)
- Traulsen C, Cornet J, Moy M and Maraninchi F A systemC/TLM semantics in PROMELA and its possible applications Proceedings of the 14th international SPIN conference on Model checking software, (204-222)
- Barnat J, Brim L and Ročkai P Scalable multi-core LTL model-checking Proceedings of the 14th international SPIN conference on Model checking software, (187-203)
- Self J and Mercer E On-the-fly dynamic dead variable analysis Proceedings of the 14th international SPIN conference on Model checking software, (113-130)
- Gueta G, Flanagan C, Yahav E and Sagiv M Cartesian partial-order reduction Proceedings of the 14th international SPIN conference on Model checking software, (95-112)
- Yang Y, Chen X, Gopalakrishnan G and Kirby R Distributed dynamic partial order reduction based verification of threaded software Proceedings of the 14th international SPIN conference on Model checking software, (58-75)
- Ruys T and de Brugh N (2007). MMC, Electronic Notes in Theoretical Computer Science (ENTCS), 190:1, (149-160), Online publication date: 1-Jul-2007.
- McGeachie J and Dingel J (2007). Translate One, Analyze Many, Electronic Notes in Theoretical Computer Science (ENTCS), 190:1, (3-18), Online publication date: 1-Jul-2007.
- Blieberger J, Burgstaller B and Mittermayr R Static detection of Livelocks in Ada multitasking programs Proceedings of the 12th international conference on Reliable software technologies, (69-83)
- Ben-Ari M (2007). Teaching concurrency and nondeterminism with spin, ACM SIGCSE Bulletin, 39:3, (363-364), Online publication date: 25-Jun-2007.
- Ben-Ari M Teaching concurrency and nondeterminism with spin Proceedings of the 12th annual SIGCSE conference on Innovation and technology in computer science education, (363-364)
- Killian C, Anderson J, Braud R, Jhala R and Vahdat A Mace Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation, (179-188)
- Ramanathan M, Grama A and Jagannathan S Static specification inference using predicate mining Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation, (123-134)
- Killian C, Anderson J, Braud R, Jhala R and Vahdat A (2007). Mace, ACM SIGPLAN Notices, 42:6, (179-188), Online publication date: 10-Jun-2007.
- Ramanathan M, Grama A and Jagannathan S (2007). Static specification inference using predicate mining, ACM SIGPLAN Notices, 42:6, (123-134), Online publication date: 10-Jun-2007.
- Gallasch G, Billington J, Vanit-Anunchai S and Kristensen L (2007). Checking safety properties on-the-fly with the sweep-line method, International Journal on Software Tools for Technology Transfer (STTT), 9:3-4, (371-391), Online publication date: 1-Jun-2007.
- Reynolds P, Spiegel M, Liu X and Gore R Validating Evolving Simulations in COERCE Proceedings of the 7th international conference on Computational Science, Part I: ICCS 2007, (1238-1245)
- Honiden S, Tahara Y, Yoshioka N, Taguchi K and Washizaki H Top SE Proceedings of the 29th international conference on Software Engineering, (708-718)
- Groce A, Holzmann G and Joshi R Randomized Differential Testing as a Prelude to Formal Verification Proceedings of the 29th international conference on Software Engineering, (621-631)
- Ramanathan M, Grama A and Jagannathan S Path-Sensitive Inference of Function Precedence Protocols Proceedings of the 29th international conference on Software Engineering, (240-250)
- Saha I and Mukhopadhyay D A distributed algorithm of fault recovery for stateful failover Proceedings of the 4th international conference on Theory and applications of models of computation, (738-749)
- Chen Z and Fickas S Do No Harm Proceedings of the 1st International Workshop on Software Engineering for Pervasive Computing Applications, Systems, and Environments
- Ermagan V, Mizutani J, Oguchi K and Weir D Towards Model-Based Failure-Management for Automotive Software Proceedings of the 4th International Workshop on Software Engineering for Automotive Systems
- Goldsby H, Knoester D, Cheng B, McKinley P and Ofria C Digitally Evolving Models for Dynamically Adaptive Systems Proceedings of the 2007 International Workshop on Software Engineering for Adaptive and Self-Managing Systems
- Ahmed T and Tripathi A (2007). Specification and verification of security requirements in a programming model for decentralized CSCW systems, ACM Transactions on Information and System Security, 10:2, (7-es), Online publication date: 1-May-2007.
- Tsay Y, Chen Y, Tsai M, Wu K and Chan W GOAL Proceedings of the 13th international conference on Tools and algorithms for the construction and analysis of systems, (466-471)
- Sebastiani R, Tonetta S and Vardi M Property-driven partitioning for abstraction refinement Proceedings of the 13th international conference on Tools and algorithms for the construction and analysis of systems, (389-404)
- Kofron J Checking software component behavior using behavior protocols and spin Proceedings of the 2007 ACM symposium on Applied computing, (1513-1517)
- Ploeger B and Somers L Analysis and verification of an automatic document feeder Proceedings of the 2007 ACM symposium on Applied computing, (1499-1505)
- Basin D, Kuruma H, Miyazaki K, Takaragi K and Wolff B (2007). Verifying a signature architecture: a comparative case study, Formal Aspects of Computing, 19:1, (63-91), Online publication date: 1-Mar-2007.
- Matousek T and Zavoral F Extracting Zing Models from C Source Code Proceedings of the 33rd conference on Current Trends in Theory and Practice of Computer Science, (900-910)
- Choi Y Checking Interaction Consistency in MARMOT Component Refinements Proceedings of the 33rd conference on Current Trends in Theory and Practice of Computer Science, (832-843)
- Brim L and Křetínský M Model-Checking Large Finite-State Systems and Beyond Proceedings of the 33rd conference on Current Trends in Theory and Practice of Computer Science, (9-28)
- Chen Z, Li X, Liu Z, Stolz V and Yang L Harnessing rCOS for tool support Formal methods and hybrid real-time systems, (83-114)
- Größer M, Norman G, Baier C, Ciesinski F, Kwiatkowska M and Parker D On reduction criteria for probabilistic reward models Proceedings of the 26th international conference on Foundations of Software Technology and Theoretical Computer Science, (309-320)
- Zave P and Cheung E Compositional control of IP media Proceedings of the 2006 ACM CoNEXT conference, (1-12)
- Baldoni M, Baroglio C, Martelli A and Patti V A priori conformance verification for guaranteeing interoperability in open environments Proceedings of the 4th international conference on Service-Oriented Computing, (339-351)
- Zhao X, Long Q and Qiu Z Model checking dynamic UML consistency Proceedings of the 8th international conference on Formal Methods and Software Engineering, (440-459)
- Yang H, Zhao X, Qiu Z, Cai C and Pu G Type checking choreography description language Proceedings of the 8th international conference on Formal Methods and Software Engineering, (264-283)
- Elamkulam J, Glazberg Z, Rabinovitz I, Kowlali G, Gupta S, Kohli S, Dattathrani S and Macia C Detecting design flaws in UML state charts for embedded software Proceedings of the 2nd international Haifa verification conference on Hardware and software, verification and testing, (109-121)
- Niebert P and Qu H The implementation of mazurkiewicz traces in POEM Proceedings of the 4th international conference on Automated Technology for Verification and Analysis, (508-522)
- Kupferman O and Lampert R On the construction of fine automata for safety properties Proceedings of the 4th international conference on Automated Technology for Verification and Analysis, (110-124)
- Madl G, Pasricha S, Bathen L, Dutt N and Zhu Q Formal performance evaluation of AMBA-based system-on-chip designs Proceedings of the 6th ACM & IEEE International conference on Embedded software, (311-320)
- Gebremichael B, Vaandrager F and Zhang M Analysis of the zeroconf protocol using UPPAAL Proceedings of the 6th ACM & IEEE International conference on Embedded software, (242-251)
- Aljazzar H and Leue S Extended directed search for probabilistic timed reachability Proceedings of the 4th international conference on Formal Modeling and Analysis of Timed Systems, (33-51)
- Edelkamp S, Jabbar S and Lafuente A Heuristic search for the analysis of graph transition systems Proceedings of the Third international conference on Graph Transformations, (414-429)
- Pesic M and van der Aalst W A declarative approach for flexible business processes management Proceedings of the 2006 international conference on Business Process Management Workshops, (169-180)
- Rensink A Model checking quantified computation tree logic Proceedings of the 17th international conference on Concurrency Theory, (110-125)
- Leue S, Ştefănescu A and Wei W A livelock freedom analysis for infinite state asynchronous reactive systems Proceedings of the 17th international conference on Concurrency Theory, (79-94)
- Saha I and Roy S A finite state modeling of AFDX frame management using spin Proceedings of the 11th international workshop, FMICS 2006 and 5th international workshop, PDMC conference on Formal methods: Applications and technology, (227-243)
- Hammer M and Weber M "To store or not to store" reloaded Proceedings of the 11th international workshop, FMICS 2006 and 5th international workshop, PDMC conference on Formal methods: Applications and technology, (51-66)
- Brim L Distributed verification Proceedings of the 11th international workshop, FMICS 2006 and 5th international workshop, PDMC conference on Formal methods: Applications and technology, (23-34)
- Ding Y and Zhang Y A case study for CTL model update Proceedings of the First international conference on Knowledge Science, Engineering and Management, (88-101)
- Tronci E (2006). Introductory Paper, International Journal on Software Tools for Technology Transfer (STTT), 8:4-5, (355-358), Online publication date: 1-Aug-2006.
- Yorsh G, Ball T and Sagiv M Testing, abstraction, theorem proving Proceedings of the 2006 international symposium on Software testing and analysis, (145-156)
- Bucchiarone A, Polini A, Pelliccione P and Tivoli M Towards an architectural approach for the dynamic and automatic composition of software components Proceedings of the ISSTA 2006 workshop on Role of software architecture for testing and analysis, (12-21)
- Donaldson A and Miller A A computational group theoretic symmetry reduction package for the SPIN model checker Proceedings of the 11th international conference on Algebraic Methodology and Software Technology, (374-380)
- Ding J, Clarke P, Xu D, He X and Deng Y (2006). A formal model-based approach for developing an interoperable mobile agent system, Multiagent and Grid Systems, 2:4, (401-412), Online publication date: 1-Jul-2006.
- Mongiello M (2006). Finite-state verification of the ebXML protocol, Electronic Commerce Research and Applications, 5:2, (147-169), Online publication date: 1-Jul-2006.
- Bucchiarone A, Muccini H and Pelliccione P A practical architecture-centric analysis process Proceedings of the Second international conference on Quality of Software Architectures, (127-144)
- Poizat P, Royer J and Salaün G Bounded analysis and decomposition for behavioural descriptions of components Proceedings of the 8th IFIP WG 6.1 international conference on Formal Methods for Open Object-Based Distributed Systems, (33-47)
- Dai L and Cooper K (2006). Modeling and performance analysis for security aspects, Science of Computer Programming, 61:1, (58-71), Online publication date: 1-Jun-2006.
- Collette S, Raskin J and Servais F On the symbolic computation of the hardest configurations of the RUSH HOUR game Proceedings of the 5th international conference on Computers and games, (220-233)
- Yin X The echo approach to formal verification Proceedings of the 28th international conference on Software engineering, (981-984)
- Autili M, Inverardi P and Pelliccione P A scenario based notation for specifying temporal properties Proceedings of the 2006 international workshop on Scenarios and state machines: models, algorithms, and tools, (21-28)
- Ding Y and Zhang Y CTL Model Update Proceedings of the 2006 conference on ECAI 2006: 17th European Conference on Artificial Intelligence August 29 -- September 1, 2006, Riva del Garda, Italy, (362-366)
- Hoffmann J, Edelkamp S, Thiébaux S, Englert R, dos Santos Liporace F and Trüg S (2006). Engineering benchmarks for planning, Journal of Artificial Intelligence Research, 26:1, (453-541), Online publication date: 1-May-2006.
- Gopalakrishnan G and Kirby R Toward reliable and efficient message passing software through formal analysis Proceedings of the 20th international conference on Parallel and distributed processing, (284-284)
- Loyauté G, Forax R and Roussel G Saburo, a tool for I/O and concurrency management in servers Proceedings of the 20th international conference on Parallel and distributed processing, (233-233)
- Joubert C and Mateescu R Distributed on-the-fly model checking and test case generation Proceedings of the 13th international conference on Model Checking Software, (126-145)
- Kupferschmid S, Hoffmann J, Dierks H and Behrmann G Adapting an AI planning heuristic for directed model checking Proceedings of the 13th international conference on Model Checking Software, (35-52)
- Kastenberg H and Rensink A Model checking dynamic states in GROOVE Proceedings of the 13th international conference on Model Checking Software, (299-305)
- Bošnački D, Leue S and Lafuente A Partial-Order reduction for general state exploring algorithms Proceedings of the 13th international conference on Model Checking Software, (271-287)
- Păsăreanu C and Giannakopoulou D Towards a compositional SPIN Proceedings of the 13th international conference on Model Checking Software, (234-251)
- Kloetzer M and Belta C A fully automated framework for control of linear systems from LTL specifications Proceedings of the 9th international conference on Hybrid Systems: computation and control, (333-347)
- Groce A and Joshi R Exploiting traces in program analysis Proceedings of the 12th international conference on Tools and Algorithms for the Construction and Analysis of Systems, (379-393)
- Kerjean S, Kabanza F, St-Denis R and Thiébaux S (2006). Analyzing LTL Model Checking Techniques for Plan Synthesis and Controller Synthesis (Work in Progress), Electronic Notes in Theoretical Computer Science (ENTCS), 149:2, (91-104), Online publication date: 1-Feb-2006.
- Mehler T and Edelkamp S (2006). Dynamic Incremental Hashing in Program Model Checking, Electronic Notes in Theoretical Computer Science (ENTCS), 149:2, (51-69), Online publication date: 1-Feb-2006.
- Edelkamp S and Jabbar S (2006). Action Planning for Directed Model Checking of Petri Nets, Electronic Notes in Theoretical Computer Science (ENTCS), 149:2, (3-18), Online publication date: 1-Feb-2006.
- Jaffar J, Santosa A and Voicu R A CLP method for compositional and intermittent predicate abstraction Proceedings of the 7th international conference on Verification, Model Checking, and Abstract Interpretation, (17-32)
- Fantechi A, Gnesi S and Semini L Achieving fault tolerance by a formally validated interaction policy Rigorous Development of Complex Fault-Tolerant Systems, (133-152)
- Combi C and Rossato R Temporal constraints with multiple granularities in smart homes Designing Smart Homes, (35-56)
- Parastatidis S, Woodman S, Webber J, Kuo D and Greenfield P (2006). Asynchronous Messaging between Web Services Using SSDL, IEEE Internet Computing, 10:1, (26-39), Online publication date: 1-Jan-2006.
- Bultan T, Su J and Fu X (2006). Analyzing Conversations of Web Services, IEEE Internet Computing, 10:1, (18-25), Online publication date: 1-Jan-2006.
- Ding Y and Zhang Y Model updating CTL systems Proceedings of the 18th Australian Joint conference on Advances in Artificial Intelligence, (5-16)
- Fu X, Bultan T and Su J (2005). Synchronizability of Conversations among Web Services, IEEE Transactions on Software Engineering, 31:12, (1042-1055), Online publication date: 1-Dec-2005.
- Oleshchuk V (2005). Modeling, specification and verification of ad-hoc sensor networks using SPIN, Computer Standards & Interfaces, 28:2, (159-165), Online publication date: 1-Dec-2005.
- Haydar M, Boroday S, Petrenko A and Sahraoui H Properties and scopes in web model checking Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering, (400-404)
- Juarez Dominguez A and Day N Compositional reasoning for port-based distributed systems Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering, (376-379)
- Kashyap S and Garg V Exploiting predicate structure for efficient reachability detection Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering, (4-13)
- Ankolekar A, Paolucci M and Sycara K Towards a formal verification of OWL-S process models Proceedings of the 4th international conference on The Semantic Web, (37-51)
- Barnat J, Brim L and Černá I Cluster-Based LTL model checking of large systems Proceedings of the 4th international conference on Formal Methods for Components and Objects, (259-279)
- Habibi A and Tahar S An approach for the verification of systemc designs using asml Proceedings of the Third international conference on Automated Technology for Verification and Analysis, (69-83)
- Della Penna G, Melatti I, Intrigila B and Tronci E Exploiting hub states in automatic verification Proceedings of the Third international conference on Automated Technology for Verification and Analysis, (54-68)
- Konrad S and Cheng B Automated analysis of natural language properties for UML models Proceedings of the 2005 international conference on Satellite Events at the MoDELS, (48-57)
- Wibling O, Parrow J and Pears A Ad hoc routing protocol verification through broadcast abstraction Proceedings of the 25th IFIP WG 6.1 international conference on Formal Techniques for Networked and Distributed Systems, (128-142)
- Aljazzar H, Hermanns H and Leue S Counterexamples for timed probabilistic reachability Proceedings of the Third international conference on Formal Modeling and Analysis of Timed Systems, (177-195)
- Tsai W, Song W, Chen Y and Paul R Dynamic system reconfiguration via service composition for dependable computing Proceedings of the 12th Monterey conference on Reliable systems on unreliable networked platforms, (203-224)
- Esterline A, Gandluri B and Sundaresan M Characterizing environmental information for monitoring agents Proceedings of the Second international conference on Radical Agent Concepts: innovative Concepts for Autonomic and Agent-Based Systems, (74-85)
- Bertolino A, Bucchiarone A, Gnesi S and Muccini H An architecture-centric approach for producing quality systems Proceedings of the First international conference on Quality of Software Architectures and Software Quality, and Proceedings of the Second International conference on Software Quality, (21-37)
- Jones V, Rensink A and Brinksma E Modelling mobile health systems Proceedings of the Ninth IEEE International EDOC Enterprise Computing Conference, (58-69)
- Molina-Jimenez C, Shrivastava S and Warne J A Method for Specifying Contract Mediated Interactions Proceedings of the Ninth IEEE International EDOC Enterprise Computing Conference, (106-118)
- Ding Y and Zhang Y Algorithms for CTL system modification Proceedings of the 9th international conference on Knowledge-Based Intelligent Information and Engineering Systems - Volume Part II, (1000-1006)
- Loer K and Harrison M Analysing user confusion in context aware mobile applications Proceedings of the 2005 IFIP TC13 international conference on Human-Computer Interaction, (184-197)
- Regayeg A, Kacem A and Jmaiel M Towards a formal methodology for designing multi-agent applications Proceedings of the Third German conference on Multiagent System Technologies, (153-164)
- Pu F, Zhang W and Wang S An improved case-based approach to LTL model checking Proceedings of the Second international conference on Rapid Integration of Software Engineering Techniques, (190-202)
- Subramaniam M and Shi J Using Dominators to Extract Observable Protocol Contexts Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods, (96-105)
- Inverardi P, Muccini H and Pelliccione P CHARMY Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, (111-114)
- de la Cámara P, Gallardo M, Merino P and Sanán D Model checking software with well-defined APIs Proceedings of the 10th international workshop on Formal methods for industrial critical systems, (17-26)
- Baier C, Ciesinski F and Groesser M Quantitative analysis of distributed randomized protocols Proceedings of the 10th international workshop on Formal methods for industrial critical systems, (2-7)
- Inverardi P, Muccini H and Pelliccione P (2005). CHARMY, ACM SIGSOFT Software Engineering Notes, 30:5, (111-114), Online publication date: 1-Sep-2005.
- Leue S and Wei W Counterexample-based refinement for a boundedness test for CFSM languages Proceedings of the 12th international conference on Model Checking Software, (58-74)
- Musuvathi M and Dill D An incremental heap canonicalization algorithm Proceedings of the 12th international conference on Model Checking Software, (28-42)
- Holzmann G and Ruys T Effective bug hunting with spin and modex Proceedings of the 12th international conference on Model Checking Software, (24-24)
- Madhavapeddy A, Scott D and Sharp R SPLAT Proceedings of the 12th international conference on Model Checking Software, (277-281)
- Donaldson A and Gay S ETCH Proceedings of the 12th international conference on Model Checking Software, (266-271)
- Rothmaier G, Kneiphoff T and Krumm H Using SPIN and eclipse for optimized high-level modeling and analysis of computer network attack models Proceedings of the 12th international conference on Model Checking Software, (236-250)
- Couvreur J, Duret-Lutz A and Poitrenaud D On-the-fly emptiness checks for generalized büchi automata Proceedings of the 12th international conference on Model Checking Software, (169-184)
- Bošnački D and Holzmann G Improving spin's partial-order reduction for breadth-first search Proceedings of the 12th international conference on Model Checking Software, (91-105)
- Donaldson A and Miller A Automatic symmetry detection for model checking using computational group theory Proceedings of the 2005 international conference on Formal Methods, (481-496)
- Hermanns H, Jansen D and Usenko Y From StoCharts to MoDeST Proceedings of the 5th international workshop on Software and performance, (13-23)
- Sebastiani R, Tonetta S and Vardi M Symbolic systems, explicit properties Proceedings of the 17th international conference on Computer Aided Verification, (350-363)
- Hoffmann J and Edelkamp S (2005). The deterministic part of IPC-4, Journal of Artificial Intelligence Research, 24:1, (519-579), Online publication date: 1-Jul-2005.
- Boroday S, Petrenko A, Singh J and Hallal H (2005). Dynamic analysis of java applications for multithreaded antipatterns, ACM SIGSOFT Software Engineering Notes, 30:4, (1-7), Online publication date: 1-Jul-2005.
- Madhavapeddy A and Scott D On the challenge of delivering high-performance, dependable, model-checked internet servers Proceedings of the First conference on Hot topics in system dependability, (6-6)
- Li X, Hu J, Bu L, Zhao J and Zheng G Consistency checking of concurrent models for scenario-based specifications Proceedings of the 12th international conference on Model Driven, (298-312)
- Hennicker R and Ludwig M Property-driven development of a coordination model for distributed simulations Proceedings of the 7th IFIP WG 6.1 international conference on Formal Methods for Open Object-Based Distributed Systems, (290-305)
- Deutsch A, Marcus M, Sui L, Vianu V and Zhou D A verifier for interactive, data-driven web applications Proceedings of the 2005 ACM SIGMOD international conference on Management of data, (539-550)
- Geilen M, Basten T and Stuijk S Minimising buffer requirements of synchronous dataflow graphs with model checking Proceedings of the 42nd annual Design Automation Conference, (819-824)
- Gruhn V and Schäfer C Architecture description for mobile distributed systems Proceedings of the 2nd European conference on Software Architecture, (239-246)
- Hull R and Su J (2005). Tools for composite web services, ACM SIGMOD Record, 34:2, (86-95), Online publication date: 1-Jun-2005.
- Ding Y and Zhang Y A logic approach for LTL system modification Proceedings of the 15th international conference on Foundations of Intelligent Systems, (435-444)
- Boroday S, Petrenko A, Singh J and Hallal H Dynamic analysis of java applications for multithreaded antipatterns Proceedings of the third international workshop on Dynamic analysis, (1-7)
- ter Beek M, Massink M, Latella D, Gnesi S, Forghieri A and Sebastianis M A case study on the automated verification of groupware protocols Proceedings of the 27th international conference on Software engineering, (596-603)
- Konrad S and Cheng B Real-time specification patterns Proceedings of the 27th international conference on Software engineering, (372-381)
- Beyer D, Henzinger T, Jhala R and Majumdar R Checking memory safety with blast Proceedings of the 8th international conference, held as part of the joint European Conference on Theory and Practice of Software conference on Fundamental Approaches to Software Engineering, (2-18)
- Balsara Z and Roach S Prediction of inherited and genetic mutations using the software model checker SPIN Proceedings of the 2005 ACM symposium on Applied computing, (208-209)
- Baier C, Ciesinski F and Größer M (2005). ProbMela and verification of Markov decision processes, ACM SIGMETRICS Performance Evaluation Review, 32:4, (22-27), Online publication date: 1-Mar-2005.
- Cortellessa V, Di Marco A, Inverardi P, Mancinelli F and Pelliccione P (2005). A Framework for the Integration of Functional and Non-functional Analysis of Software Architectures, Electronic Notes in Theoretical Computer Science (ENTCS), 116:C, (31-44), Online publication date: 19-Jan-2005.
- Gyapay S and Pataricza A (2005). Optimal trajectory generation for petri nets, Acta Cybernetica, 17:2, (225-245), Online publication date: 10-Jan-2005.
- He Y and Janicki R Verifying protocols by model checking Proceedings of the 2004 conference of the Centre for Advanced Studies on Collaborative research, (174-188)
- Michell S and Srinivasan K State based key hop protocol Proceedings of the 1st ACM international workshop on Performance evaluation of wireless ad hoc, sensor, and ubiquitous networks, (112-118)
- Henderson P, Walters R and Crouch S Implementing Hierarchical Features in a Graphically Based Formal Modelling Language Proceedings of the 28th Annual International Computer Software and Applications Conference - Volume 01, (92-98)
- Haydar M Formal Framework for Automated Analysis and Verification of Web-Based Applications Proceedings of the 19th IEEE international conference on Automated software engineering, (410-413)
- Ben-Ari M (2004). A suite of tools for teaching concurrency, ACM SIGCSE Bulletin, 36:3, (251-251), Online publication date: 1-Sep-2004.
- Koshkina M and van Breugel F (2004). Modelling and verifying web service orchestration by means of the concurrency workbench, ACM SIGSOFT Software Engineering Notes, 29:5, (1-10), Online publication date: 1-Sep-2004.
- Dwyer M and Leue S (2004). Introductory paper, International Journal on Software Tools for Technology Transfer (STTT), 6:4, (257-259), Online publication date: 1-Aug-2004.
- Edelkamp S, Leue S and Lluch-Lafuente A (2004). Partial-order reduction and trail improvement in directed model checking, International Journal on Software Tools for Technology Transfer (STTT), 6:4, (277-301), Online publication date: 1-Aug-2004.
- Walton C Model checking agent dialogues Proceedings of the Second international conference on Declarative Agent Languages and Technologies, (132-147)
- Fu X, Bultan T and Su J Model checking XML manipulating software Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, (252-262)
- Edwards J, Jackson D, Torlak E and Yeung V Faster constraint solving with subtypes Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, (232-242)
- Muñoz C, Dowek G and Carreño V Modeling and verification of an air traffic concept of operations Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, (175-182)
- Fu X, Bultan T and Su J (2004). Model checking XML manipulating software, ACM SIGSOFT Software Engineering Notes, 29:4, (252-262), Online publication date: 1-Jul-2004.
- Edwards J, Jackson D, Torlak E and Yeung V (2004). Faster constraint solving with subtypes, ACM SIGSOFT Software Engineering Notes, 29:4, (232-242), Online publication date: 1-Jul-2004.
- Muñoz C, Dowek G and Carreño V (2004). Modeling and verification of an air traffic concept of operations, ACM SIGSOFT Software Engineering Notes, 29:4, (175-182), Online publication date: 1-Jul-2004.
- Ben-Ari M A suite of tools for teaching concurrency Proceedings of the 9th annual SIGCSE conference on Innovation and technology in computer science education, (251-251)
- Bošnački D Black box checking for biochemical networks Proceedings of the 20 international conference on Computational Methods in Systems Biology, (225-230)
- Tan J, Avrunin G and Clarke L Heuristic-Based Model Refinement for FLAVERS Proceedings of the 26th International Conference on Software Engineering, (635-644)
- Caporuscio M, Inverardi P and Pelliccione P Compositional Verification of Middleware-Based Software Architecture Descriptions Proceedings of the 26th International Conference on Software Engineering, (221-230)
- Fu X, Bultan T and Su J Analysis of interacting BPEL web services Proceedings of the 13th international conference on World Wide Web, (621-630)
- Michaelson G, Hammond K and Serot J FSM-Hume Proceedings of the 2004 ACM symposium on Applied computing, (1455-1461)
- Hartel P, van Eck P, Etalle S and Wieringa R Modelling mobility aspects of security policies Proceedings of the 2004 international conference on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, (172-191)
- Formal methods and software reliability Proceedings of the Second ACM/IEEE International Conference on Formal Methods and Models for Co-Design, (145-146)
- Regan P and Hamilton S (2004). NASA's Mission Reliable, Computer, 37:1, (59-68), Online publication date: 1-Jan-2004.
- Ruys T Optimal scheduling using branch and bound with SPIN 4.0 Proceedings of the 10th international conference on Model checking software, (1-17)
- Gallardo M, Luque-Schempp F, Merino-Gómez P and Panizo L How Formal Methods Can Contribute to 5G Networks From Software Engineering to Formal Methods and Tools, and Back, (548-571)
Recommendations
The software model checker Blast: Applications to software engineering
Blast is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, Blast either statically proves that the program satisfies the safety property, or provides an execution path ...
The software model checker Blast
Blast is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, Blast either statically proves that the program satisfies the safety property, or provides an execution path ...
The SpinJa model checker
SPIN'10: Proceedings of the 17th international SPIN conference on Model checking softwareSPINJA is a model checker for PROMELA, implemented in Java. SPINJA is designed to behave similarly to SPIN, but to be more easily extendible and reusable. Despite the fact that SPINJA uses a layered object-oriented design and is written in Java, SPINJA'...