Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
137 | Alastair F. Donaldson, Alice Miller 0001 |
Automatic Symmetry Detection for Promela. |
J. Autom. Reason. |
2008 |
DBLP DOI BibTeX RDF |
Model checking, Automatic verification, Symmetry reduction, Promela |
100 | Moataz Kamel, Stefan Leue |
VIP: A Visual Editor and Compiler for v-Promela. |
TACAS |
2000 |
DBLP DOI BibTeX RDF |
|
88 | Stefan Leue, Richard Mayr, Wei Wei 0015 |
A Scalable Incomplete Test for Message Buffer Overflow in Promela Models. |
SPIN |
2004 |
DBLP DOI BibTeX RDF |
|
73 | Moataz Kamel, Stefan Leue |
Formalization and Validation of the General Inter-ORB Protocol (GIOP) using PROMELA and SPIN. |
Int. J. Softw. Tools Technol. Transf. |
2000 |
DBLP DOI BibTeX RDF |
General Inter-ORB Protocol, Promela/Spin, Model checking, Temporal logic, Specification patterns |
62 | Óscar R. Ribeiro, João M. Fernandes |
Translating Synchronous Petri Nets into PROMELA for Verifying Behavioural Properties. |
SIES |
2007 |
DBLP DOI BibTeX RDF |
|
62 | Alastair F. Donaldson, Simon J. Gay |
Etch: An Enhanced Type Checking Tool for Promela. |
SPIN |
2005 |
DBLP DOI BibTeX RDF |
|
62 | Michael Baldamus, Jochen Schröder-Babo |
p2b: A Translation Utility for Linking Promela and Symbolic Model Checking (Tool Paper). |
SPIN |
2001 |
DBLP DOI BibTeX RDF |
|
60 | María-del-Mar Gallardo, Pedro Merino 0001, Ernesto Pimentel 0001 |
A generalized semantics of PROMELA for abstract model checking. |
Formal Aspects Comput. |
2004 |
DBLP DOI BibTeX RDF |
Model checking, Abstraction, spin, Structured operational semantics, promela |
51 | René G. de Vries, Jan Tretmans |
On-the-fly Conformance Testing using SPIN. |
Int. J. Softw. Tools Technol. Transf. |
2000 |
DBLP DOI BibTeX RDF |
Spin verification tool, Formal methods, Conformance testing, Test automation, Test generation algorithms |
51 | Klaus Havelund, Thomas Pressburger |
Model Checking JAVA Programs using JAVA PathFinder. |
Int. J. Softw. Tools Technol. Transf. |
2000 |
DBLP DOI BibTeX RDF |
Java, Model checking, Program verification, Concurrent programming, Deadlocks, Assertions, Spin |
49 | Christophe Pajault, Jean-François Pradat-Peyre, Pierre Rousseau |
Adapting Petri Nets Reductions to Promela Specifications. |
FORTE |
2008 |
DBLP DOI BibTeX RDF |
|
49 | Stefan Leue, Gerard J. Holzmann |
v-Promela: A Visual, Object-Oriented Language for SPIN. |
ISORC |
1999 |
DBLP DOI BibTeX RDF |
|
49 | Dragan Bosnacki, Dennis Dams |
Discrete-Time Promela and Spin. |
FTRTFT |
1998 |
DBLP DOI BibTeX RDF |
|
49 | Jan Kofron |
Checking software component behavior using behavior protocols and spin. |
SAC |
2007 |
DBLP DOI BibTeX RDF |
verification, behavior specification, promela, behavior protocols |
49 | Alastair F. Donaldson, Alice Miller 0001 |
Exact and Approximate Strategies for Symmetry Reduction in Model Checking. |
FM |
2006 |
DBLP DOI BibTeX RDF |
Promela/Spin, computational group theory, model checking, symmetry, Gap |
49 | Alastair F. Donaldson, Alice Miller 0001 |
Automatic Symmetry Detection for Model Checking Using Computational Group Theory. |
FM |
2005 |
DBLP DOI BibTeX RDF |
Promela /Spin, distributed systems, model checking, concurrency, formal modelling, communicating processes, Gap, symmetry reduction |
49 | Yung-Pin Cheng, Michal Young, Che-Ling Huang, Chia-Yi Pan |
Towards scalable compositional analysis by refactoring design models. |
ESEC / SIGSOFT FSE |
2003 |
DBLP DOI BibTeX RDF |
refactoring, CCS, compositional analysis, promela |
48 | Aznam Yacoub, Maâmar El-Amine Hamri, Claudia S. Frydman, Chungman Seo, Bernard P. Zeigler |
DEv-PROMELA: an extension of PROMELA for the modelling, simulation and verification of discrete-event systems. |
Int. J. Simul. Process. Model. |
2017 |
DBLP DOI BibTeX RDF |
|
47 | Jean-Charles Grégoire |
TLA + PROMELA: Conjecture, Check, Proof, Engineering New Protocols Using Methods and Formal Notations. |
FME |
1997 |
DBLP DOI BibTeX RDF |
keyword TLA+, refinement, implementation, SPIN, PROMELA, TLA |
38 | Raman Kazhamiakin, Marco Pistore, Marco Roveri |
Formal Verification of Requirements using SPIN: A Case Study on Web Services. |
SEFM |
2004 |
DBLP DOI BibTeX RDF |
|
38 | Asif Iqbal 0004, A. K. Bhattacharjee, S. D. Dhodapkar, S. Ramesh 0001 |
Visual Modeling and Verification of Distributed Reactive Systems. |
SAFECOMP |
2003 |
DBLP DOI BibTeX RDF |
|
38 | Rafael H. Bordini, Michael Fisher 0001, Willem Visser, Michael J. Wooldridge |
Verifiable Multi-agent Programs. |
PROMAS |
2003 |
DBLP DOI BibTeX RDF |
|
38 | Seung Mo Cho, Doo-Hwan Bae, Sung Deok Cha, Young Gon Kim, Byung Kyu Yoo, Sang Taek Kim |
Applying Model Checking to Concurrent Object-Oriented Software. |
ISADS |
1999 |
DBLP DOI BibTeX RDF |
|
37 | Dragan Bosnacki, Alastair F. Donaldson, Michael Leuschel, Thierry Massart |
Efficient Approximate Verification of Promela Models Via Symmetry Markers. |
ATVA |
2007 |
DBLP DOI BibTeX RDF |
|
37 | Óscar R. Ribeiro, João M. Fernandes, Luís F. Pinto |
Model Checking Embedded Systems with PROMELA. |
ECBS |
2005 |
DBLP DOI BibTeX RDF |
|
37 | Nicolas Guelfi, Amel Mammar |
A Formal Semantics of Timed Activity Diagrams and its PROMELA Translation. |
APSEC |
2005 |
DBLP DOI BibTeX RDF |
|
37 | Yung-Pin Cheng |
Crafting a Promela Front-End with Abstract Data Types to Mitigate the Sensitivity of (Compositional) Analysis to Implementation Choices. |
SPIN |
2005 |
DBLP DOI BibTeX RDF |
|
37 | Jessica Chen, Hanmei Cui |
Translation from Adapted UML to Promela for CORBA-Based Applications. |
SPIN |
2004 |
DBLP DOI BibTeX RDF |
Model Checking, UML, Middleware, CORBA, SPIN, Distributed Object Systems, Formal Specification and Verification |
37 | Stefan Edelkamp |
Promela Planning. |
SPIN |
2003 |
DBLP DOI BibTeX RDF |
|
37 | Ramazan Savas Aygün, Aidong Zhang |
Modeling and Verification of Interactive Flexible Multimedia Presentations Using PROMELA/SPIN. |
SPIN |
2002 |
DBLP DOI BibTeX RDF |
|
37 | Clement Yuen, Wei Tjioe |
Modeling and Verifying a Price Model for Congestion Control in Computer Networks Using Promela/Spin. |
SPIN |
2001 |
DBLP DOI BibTeX RDF |
|
37 | Lynette I. Millett, Tim Teitelbaum |
Issues in Slicing PROMELA and Its Applications to Model Checking, Protocol Understanding, and Simulation. |
Int. J. Softw. Tools Technol. Transf. |
2000 |
DBLP DOI BibTeX RDF |
Model checking, Static analysis, Program slicing, Concurrent languages |
37 | Carl B. Adekunle, Steve A. Schneider |
Detecting Feature Interactions in the Terrestrial Trunked Radio (TETRA) Network Using Promela and Xspin. |
SPIN |
1999 |
DBLP DOI BibTeX RDF |
|
37 | Heikki Tuominen |
Embedding a Dialect of SDL in PROMELA. |
SPIN |
1999 |
DBLP DOI BibTeX RDF |
|
37 | María-del-Mar Gallardo, Pedro Merino 0001 |
A Framework for Automatic Construction of Abstract Promela Models. |
SPIN |
1999 |
DBLP DOI BibTeX RDF |
|
37 | Erich Mikk, Yassine Lakhnech, Michael Siegel, Gerard J. Holzmann |
Implementing Statecharts in PROMELA/SPIN. |
WIFT |
1998 |
DBLP DOI BibTeX RDF |
|
36 | Sebastian Schmerl, Michael Vogel, Hartmut König |
Identifying Modeling Errors in Signatures by Model Checking. |
SPIN |
2009 |
DBLP DOI BibTeX RDF |
Attack Signatures, Intrusion Detection, Computer Security, Signature Verification, Misuse Detection, Promela, Spin model checker |
36 | Manuel J. Fernández-Iglesias, Martín Llamas Nistal |
An Undergraduate Course on Protocol Engineering - How to Teach Formal Methods Without Scaring Students. |
TFM |
2004 |
DBLP DOI BibTeX RDF |
undergraduate courses, Spin, Protocol engineering, Promela, case-based learning |
36 | Xiang Fu 0001, Tevfik Bultan, Jianwen Su |
Model checking XML manipulating software. |
ISSTA |
2004 |
DBLP DOI BibTeX RDF |
MSL, web service, XML, model checking, XPath, XML schema, SPIN, promela |
36 | Christopher P. Fuhrman |
Lightweight models for interpreting informal specifications. |
Requir. Eng. |
2003 |
DBLP DOI BibTeX RDF |
Informal specifications, Iterative software development, Lightweight models, Request for Comments (RFC), Trivial File Transfer, Protocol (TFTP)SPIN, Process, PROMELA |
36 | Muffy Calder, Alice Miller 0001 |
Using SPIN for Feature Interaction Analysis - A Case Study. |
SPIN |
2001 |
DBLP DOI BibTeX RDF |
Promela/SPIN, analysis and reasoning techniques, distributed systems, formal modelling, feature interaction, communicating processes, telecommunications services |
36 | Diego Latella, István Majzik, Mieke Massink |
Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-checker. |
Formal Aspects Comput. |
1999 |
DBLP DOI BibTeX RDF |
UML Statechart Diagrams, Model-checking, Program transformation, SPIN, PROMELA |
26 | Zuohua Ding, Mingyue Jiang, Jing Liu 0012 |
Model Checking Service Component Composition by SPIN. |
ACIS-ICIS |
2009 |
DBLP DOI BibTeX RDF |
|
26 | Tim Kovse, Bostjan Vlaovic, Aleksander Vreze, Zmago Brezocnik |
Eclipse Plug-In for Spin and st2msc Tools-Tool Presentation. |
SPIN |
2009 |
DBLP DOI BibTeX RDF |
|
26 | Christopher Power, Alice Miller 0001 |
Prism2Promela. |
QEST |
2008 |
DBLP DOI BibTeX RDF |
|
26 | Alex Groce, Rajeev Joshi |
Random testing and model checking: building a common framework for nondeterministic exploration. |
WODA |
2008 |
DBLP DOI BibTeX RDF |
model checking, dynamic analysis, random testing, test frameworks |
26 | Youssef Hanna |
SLEDE: lightweight verification of sensor network security protocol implementations. |
ESEC/SIGSOFT FSE |
2007 |
DBLP DOI BibTeX RDF |
slede, sensor networks, model checking, security protocols |
26 | Domenico Bianculli, Paola Spoletini, Angelo Morzenti, Matteo Pradella, Pierluigi San Pietro |
Model Checking Temporal Metric Specifications with Trio2Promela. |
FSEN |
2007 |
DBLP DOI BibTeX RDF |
model checking, temporal logic, Spin |
26 | Fernando Luís Dotti, Leila Ribeiro 0001, Osmar Marchi dos Santos, Fábio Pasini |
Verifying Object-based Graph Grammars. |
Softw. Syst. Model. |
2006 |
DBLP DOI BibTeX RDF |
Partial systems, Model checking, Reactive systems, Graph grammars, Object-based systems |
26 | Alastair F. Donaldson, Alice Miller 0001 |
A Computational Group Theoretic Symmetry Reduction Package for the Spin Model Checker. |
AMAST |
2006 |
DBLP DOI BibTeX RDF |
|
26 | Honghua Cao, Shi Ying, Dehui Du |
Towards Model-based Verification of BPEL with Model Checking. |
CIT |
2006 |
DBLP DOI BibTeX RDF |
|
26 | Stefan Leue, Wei Wei 0015 |
Counterexample-Based Refinement for a Boundedness Test for CFSM Languages. |
SPIN |
2005 |
DBLP DOI BibTeX RDF |
|
26 | Jesús Arias-Fisteus, Luis Sánchez Fernández 0001, Carlos Delgado Kloos |
Formal Verification of BPEL4WS Business Collaborations. |
EC-Web |
2004 |
DBLP DOI BibTeX RDF |
|
26 | Theo C. Ruys |
Optimal Scheduling Using Branch and Bound with SPIN 4.0. |
SPIN |
2003 |
DBLP DOI BibTeX RDF |
|
26 | Fernando Luís Dotti, Luciana Foss, Leila Ribeiro 0001, Osmar Marchi dos Santos |
Verification of Distributed Object-Based Systems. |
FMOODS |
2003 |
DBLP DOI BibTeX RDF |
|
26 | Ed Brinksma, Angelika Mader, Ansgar Fehnker |
Verification and optimization of a PLC control schedule. |
Int. J. Softw. Tools Technol. Transf. |
2002 |
DBLP DOI BibTeX RDF |
Scheduling, Model checking, Verification, Formal methods, Hybrid systems |
26 | Theo C. Ruys |
SPIN Tutorial: How to Become a SPIN Doctor. |
SPIN |
2002 |
DBLP DOI BibTeX RDF |
|
26 | Stefan Edelkamp, Alberto Lluch-Lafuente, Stefan Leue |
Directed Explicit Model Checking with HSF-SPIN. |
SPIN |
2001 |
DBLP DOI BibTeX RDF |
|
26 | Gerald C. Gannod, Sunil Gupta |
An Automated Tool for Analyzing Petri Nets Using SPIN. |
ASE |
2001 |
DBLP DOI BibTeX RDF |
|
26 | Dragan Bosnacki, Dennis Dams, Leszek Holenderski, Natalia Sidorova |
Model Checking SDL with Spin. |
TACAS |
2000 |
DBLP DOI BibTeX RDF |
|
24 | Natalia Olegovna Garanina, Sergey M. Staroletov, Sergei Gorlatch |
Auto-Tuning High-Performance Programs Using Model Checking in Promela. |
CoRR |
2023 |
DBLP DOI BibTeX RDF |
|
24 | Hui Feng, Marcello M. Bonsangue, Benjamin Lion |
From symbolic constraint automata to Promela. |
J. Log. Algebraic Methods Program. |
2022 |
DBLP DOI BibTeX RDF |
|
24 | Marco Comini, María-del-Mar Gallardo, Alicia Villanueva |
A denotational semantics for PROMELA addressing arbitrary jumps. |
CoRR |
2021 |
DBLP BibTeX RDF |
|
24 | Viktor Shatrov, Valeriy Vyatkin |
Promela Formal Modelling and Verification of IEC 61499 Systems with comparison to SMV. |
INDIN |
2021 |
DBLP DOI BibTeX RDF |
|
24 | Aznam Yacoub, Maâmar El-Amine Hamri, Claudia S. Frydman |
DEv-PROMELA: modeling, verification, and validation of a video game by combining model-checking and simulation. |
Simul. |
2020 |
DBLP DOI BibTeX RDF |
|
24 | Nicolas Dilley, Julien Lange |
Bounded verification of message-passing concurrency in Go using Promela and Spin. |
PLACES@ETAPS |
2020 |
DBLP DOI BibTeX RDF |
|
24 | Georgiana Caltais, Stefan Leue, Hargurbir Singh |
Correctness of an ATL Model Transformation from SysML State Machine Diagrams to Promela. |
MODELSWARD |
2020 |
DBLP DOI BibTeX RDF |
|
24 | Abdelhak Khemiri, Maâmar El-Amine Hamri, Claudia S. Frydman, Jacques Pinaton |
Limiting state space explosion of model checking using discrete event simulation: combining DEVS and PROMELA. |
SummerSim |
2019 |
DBLP BibTeX RDF |
|
24 | Massimo Benerecetti, Ugo Gentile, Stefano Marrone 0001, Roberto Nardone, Adriano Peron, Luigi L. L. Starace, Valeria Vittorini |
From Dynamic State Machines to Promela. |
SPIN |
2019 |
DBLP DOI BibTeX RDF |
|
24 | Jutamard Kawises, Wiwat Vatanawood |
Formalizing Time Petri Nets with Metric Temporal Logic using Promela. |
SNPD |
2019 |
DBLP DOI BibTeX RDF |
|
24 | Haklin Kimm, Hanke Kimm |
Modeling and Verification of Starvation-Free Bitwise Arbitration Technique for Controller Area Network Using SPIN Promela. |
IMCOM |
2019 |
DBLP DOI BibTeX RDF |
|
24 | Soufiane Zahid, Abdeslam En-Nouaary, Slimane Bah |
An SDL to Discrete-Time PROMELA Transformation of Home Area Network model. |
SITA |
2018 |
DBLP DOI BibTeX RDF |
|
24 | Benjamin Lion, Samir Chouali, Farhad Arbab |
Compiling Protocols to Promela and Verifying their LTL Properties. |
MoDELS (Workshops) |
2018 |
DBLP BibTeX RDF |
|
24 | Lamia Eljadiri, Ismail Assayad |
A platform for systematic verification of embedded components in IP-XACT, SystemC and Promela. |
ICSDE |
2018 |
DBLP DOI BibTeX RDF |
|
24 | Aznam Yacoub, Maâmar El-Amine Hamri, Claudia S. Frydman |
Restricting DEv-PROMELA with a hierarchy of simulation formalisms. |
SpringSim (TMS) |
2017 |
DBLP BibTeX RDF |
|
24 | Ryan F. Kirwan, Alice Miller 0001, Bernd Porr |
Model checking learning agent systems using Promela with embedded C code and abstraction. |
Formal Aspects Comput. |
2016 |
DBLP DOI BibTeX RDF |
|
24 | Aznam Yacoub, Maâmar El-Amine Hamri, Claudia S. Frydman |
Using DEv-PROMELA for Modelling and Verification of Software. |
SIGSIM-PADS |
2016 |
DBLP DOI BibTeX RDF |
|
24 | Maryam Dabaghchian, Mohammad Abdollahi Azgomi |
Model checking the observational determinism security property using PROMELA and SPIN. |
Formal Aspects Comput. |
2015 |
DBLP DOI BibTeX RDF |
|
24 | Roberto Nardone, Ugo Gentile, Massimo Benerecetti, Adriano Peron, Valeria Vittorini, Stefano Marrone 0001, Nicola Mazzocca |
Modeling Railway Control Systems in Promela. |
FTSCS |
2015 |
DBLP DOI BibTeX RDF |
|
24 | Annabelle Klarl |
From Helena Ensemble Specifications to Promela Verification Models. |
SPIN |
2015 |
DBLP DOI BibTeX RDF |
|
24 | Ahmad Siyar Andisha, Martin Wehrle, Bernd Westphal |
Directed Model Checking for PROMELA with Relaxation-Based Distance Functions. |
SPIN |
2015 |
DBLP DOI BibTeX RDF |
|
24 | Mirtha Lina Fernández Venero, Flávio Soares Corrêa da Silva |
A general translation from nested Petri nets into PROMELA. |
CoRR |
2014 |
DBLP BibTeX RDF |
|
24 | René Neumann |
Promela Formalization. |
Arch. Formal Proofs |
2014 |
DBLP BibTeX RDF |
|
24 | René Neumann |
Using Promela in a Fully Verified Executable LTL Model Checker. |
VSTTE |
2014 |
DBLP DOI BibTeX RDF |
|
24 | Aznam Yacoub, Maâmar El-Amine Hamri, Claudia S. Frydman |
Complementarity between simulation and formal verification transformation of PROMELA models into FDDEVS models: Application to a case study. |
SIMULTECH |
2014 |
DBLP BibTeX RDF |
|
24 | Dieu-Huong Vu, Yuki Chiba, Kenro Yatake, Toshiaki Aoki |
Checking the Conformance of a Promela Design to its Formal Specification in Event-B. |
FTSCS |
2014 |
DBLP DOI BibTeX RDF |
|
24 | Kevin Chalmers, Jon M. Kerridge |
Verifying the CPA Networking Stack using SPIN/Promela. |
CPA |
2013 |
DBLP BibTeX RDF |
|
24 | Asankhaya Sharma |
A Refinement Calculus for Promela. |
ICECCS |
2013 |
DBLP DOI BibTeX RDF |
|
24 | Freark I. van der Berg, Alfons Laarman |
SpinS: Extending LTSmin with Promela through SpinJa. |
PASM/PDMC |
2012 |
DBLP DOI BibTeX RDF |
|
24 | Leila Ribeiro 0001, Osmar Marchi dos Santos, Fernando Luís Dotti, Luciana Foss |
Correct transformation: From object-based graph grammars to PROMELA. |
Sci. Comput. Program. |
2012 |
DBLP DOI BibTeX RDF |
|
24 | Mouna Ait Oubelli, Nadia Younsi, Abdelkrim Amirat, Ahcene Menasria |
From UML 2.0 Sequence Diagrams to PROMELA code by Graph Transformation using AToM3. |
CIIA |
2011 |
DBLP BibTeX RDF |
|
24 | Bob de Vos, Lennart C. L. Kats, Cornelis Pronk |
EpiSpin: An Eclipse Plug-In for Promela/Spin Using Spoofax. |
SPIN |
2011 |
DBLP DOI BibTeX RDF |
|
24 | Yogesh Mali, Eric Van Wyk |
Building Extensible Specifications and Implementations of Promela with AbleP. |
SPIN |
2011 |
DBLP DOI BibTeX RDF |
|
24 | Daniele Campana, Alessandro Cimatti, Iman Narasamdya, Marco Roveri |
An Analytic Evaluation of SystemC Encodings in Promela. |
SPIN |
2011 |
DBLP DOI BibTeX RDF |
|
24 | Jan Staunton, John A. Clark |
Finding short counterexamples in promela models using estimation of distribution algorithms. |
GECCO |
2011 |
DBLP DOI BibTeX RDF |
|
24 | Ryosuke Nakashiro, Yasutaka Kamei, Naoyasu Ubayashi, Shin Nakajima 0001, Akihito Iwai |
Translation Pattern of BPEL Process into Promela Code. |
IWSM/Mensura |
2011 |
DBLP DOI BibTeX RDF |
|
24 | Ling Yin, Frédéric Mallet, Jing Liu 0012 |
Verification of MARTE/CCSL Time Requirements in Promela/SPIN. |
ICECCS |
2011 |
DBLP DOI BibTeX RDF |
|
24 | Vincent Beaudenon, Emmanuelle Encrenaz, Sami Taktak |
Data decision diagrams for Promela systems analysis. |
Int. J. Softw. Tools Technol. Transf. |
2010 |
DBLP DOI BibTeX RDF |
|
24 | Alastair F. Donaldson, Simon J. Gay |
Type inference and strong static type checking for Promela. |
Sci. Comput. Program. |
2010 |
DBLP DOI BibTeX RDF |
|
24 | Andreas Ulrich, El Hachemi Alikacem, Hesham Hallal, Sergiy Boroday |
From Scenarios to Test Implementations Via Promela. |
ICTSS |
2010 |
DBLP DOI BibTeX RDF |
|