Search results for "S-TLA "

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
228	Leslie Lamport	Distributed algorithms in TLA (abstract).	PODC	2000	DBLP DOI BibTeX RDF
95	Hehua Zhang, Stephan Merz, Ming Gu 0001	Specifying and Verifying PLC Systems with TLA+.	TASE	2009	DBLP DOI BibTeX RDF
95	Yuan Yu, Panagiotis Manolios, Leslie Lamport	Model Checking TLA+ Specifications.	CHARME	1999	DBLP DOI BibTeX RDF
82	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
80	Ondrej Rysavý, Jaroslav Ráb	A formal model of composing components: the TLA+ approach.	Innov. Syst. Softw. Eng.	2009	DBLP DOI BibTeX RDF	Composing specifications, Synchronous mode of executions, Temporal logic of actions, Component model, Hierarchical specifications
80	Nasreddine Aoumeur, Kamel Barkaoui, Gunter Saake	Towards Maude-Tla based Foundation for Complex Concurrent Systems Specification and Certification.	ITNG	2008	DBLP DOI BibTeX RDF
74	Rajeev Joshi, Leslie Lamport, John Matthews, Serdar Tasiran, Mark R. Tuttle, Yuan Yu	Checking Cache-Coherence Protocols with TLA+.	Formal Methods Syst. Des.	2003	DBLP DOI BibTeX RDF	TLC, model checking, cache coherence, TLA+
74	Leslie Lamport	The Temporal Logic of Actions.	ACM Trans. Program. Lang. Syst.	1994	DBLP DOI BibTeX RDF	concurrent programming, safety properties, liveness properties
68	Jan Täubrich, Reinhard von Hanxleden	Formal Specification and Analysis of AFDX Redundancy Management Algorithms.	SAFECOMP	2007	DBLP DOI BibTeX RDF	Redundancy Management, AFDX, Model Checking, Case Study, TLA
68	Bo Wang, Cornelis Pronk	Design and implementation of a GUI for the TLC model checker.	ACM SIGPLAN Notices	2006	DBLP DOI BibTeX RDF	GraphViz, TLC, model checking, GUI, temporal logic, SML, TLA+
66	Peter B. Ladkin, Leslie Lamport, Bryan Olivier, Denis Roegel	Lazy Caching in TLA.	Distributed Comput.	1999	DBLP DOI BibTeX RDF
66	Dominique Cansell, Dominique Méry	Abstract Animator for Temporal Specifications: Application to TLA.	SAS	1999	DBLP DOI BibTeX RDF
66	Abdelillah Mokkedem, Michael J. Ferguson, Robert de B. Johnston	A TLA Solution to the Specification and Verification of the RLP1 Retransmission Protocol.	FME	1997	DBLP DOI BibTeX RDF
53	Reino Kurki-Suonio	Action systems in incremental and aspect-oriented modeling.	Distributed Comput.	2003	DBLP DOI BibTeX RDF	Incremental modeling, Formal specification, Aspects, Action systems, Superposition, TLA
51	Yassin Mokhtari, Stephan Merz	Animating TLA Specifications.	LPAR	1999	DBLP DOI BibTeX RDF
45	Hui Kong 0004, Hehua Zhang, Xiaoyu Song, Ming Gu 0001, Jiaguang Sun 0001	Proving Computational Geometry Algorithms in TLA+2.	TASE	2011	DBLP DOI BibTeX RDF	algorithm verification, TLA+2, geometry algorithm, theorem proving, loop invariant
45	Hongbing Wang, Qianzhao Zhou, Yanqi Shi	Describing and Verifying Web Service Composition Using TLA Reasoning.	IEEE SCC	2010	DBLP DOI BibTeX RDF	Web service, service composition, OWL-S, verifying, TLA
45	Shuai Luan, Yuliang Shi, Haiyang Wang	A Mechanism of Modeling and Verification for SaaS Customization Based on TLA.	WISM	2009	DBLP DOI BibTeX RDF	Verification, Customization, SaaS, TLA
45	Guodong Li, Michael Delisi, Ganesh Gopalakrishnan, Robert M. Kirby	Formal specification of the MPI-2.0 standard in TLA+.	PPoPP	2008	DBLP DOI BibTeX RDF	model checking, formal specification, MPI, TLA+
44	Slim Rekhis, Noureddine Boudriga	A Temporal Logic-Based Model for Forensic Investigation in Networked System Security.	MMM-ACNS	2005	DBLP DOI BibTeX RDF
44	Robert Chebli, Abdallah Kassem, Mohamad Sawan	Logarithmic programmable preamplifier dedicated to ultrasonic receivers.	ISCAS (1)	2002	DBLP DOI BibTeX RDF
44	Paulo Nazareno Maia Sampaio, Jean-Pierre Courtiat	Scheduling and Presenting Interactive Multimedia Documents.	ICME	2001	DBLP DOI BibTeX RDF
44	Denis Roegel	Specifying Almost-Real Concurrent Object-Oriented Programs.	PDP	1996	DBLP DOI BibTeX RDF	almost-real concurrent object-oriented programs, refinement chain, CTLA, structuring concerns, formal specification, parallel programming, parallel programming, object-oriented programming, specification, specification languages
44	Todd Fine	Defining Noninterference in the Temporal Logic of Actions.	S&P	1996	DBLP DOI BibTeX RDF	noninterference properties, temporal logic of actions, multilevel secure systems, formal specification, formal methods, temporal logic, composition, security of data, covert channels, definitions, specification refinement
44	Joakim von Wright, Thomas Långbacka	Using a Theorem Prover for Reasoning about Concurrent Algorithms.	CAV	1992	DBLP DOI BibTeX RDF
43	Antoine Defourné	Encodages de la théorie des ensembles de TLA+ pour la preuve automatique. (Encoding TLA+'s Set Theory for Automated Theorem Provers).		2023	RDF
43	Jure Kukovec, Thanh-Hai Tran 0002, Igor Konnov 0001	Extracting Symbolic Transitions from TLA+ Specifications.	ABZ	2018	DBLP DOI BibTeX RDF
43	Florent Chevrou, Aurélie Hurault, Philippe Mauran, Philippe Quéinnec	Mechanized Refinement of Communication Models with TLA ^+ +.	ABZ	2016	DBLP DOI BibTeX RDF
43	Stephan Merz, Hernán Vanzetto	Encoding TLA ^+ + into Many-Sorted First-Order Logic.	ABZ	2016	DBLP DOI BibTeX RDF
43	Hernán Vanzetto	Proof automation and type synthesis for set theory in the context of TLA+. (Automatisation de preuves et synthèse de types pour la théorie des ensembles dans le contexte de TLA+).		2014	RDF
43	Chris Newcombe	Why Amazon Chose TLA +.	ABZ	2014	DBLP DOI BibTeX RDF
43	Dominik Hansen, Michael Leuschel	Translating B to TLA + for Validation with TLC.	ABZ	2014	DBLP DOI BibTeX RDF
38	Ariel Cohen 0002, John W. O'Leary, Amir Pnueli, Mark R. Tuttle, Lenore D. Zuck	Verifying Correctness of Transactional Memories.	FMCAD	2007	DBLP DOI BibTeX RDF	HTM, STM, TLC, model checking, Verification, transactional memory, TLA+
38	Slim Rekhis, Noureddine Boudriga	A formal logic-based language and an automated verification tool for computer forensic investigation.	SAC	2005	DBLP DOI BibTeX RDF	S-TLA+, S-TLC, formal forensic investigation, temporal logic of security actions
38	Peter Baumann, Karl Lermer	A Framework for the Specification of Reactive and Concurrent Systems in Z.	FSTTCS	1995	DBLP DOI BibTeX RDF	formal methods, reactive systems, Z, TLA
36	Hongbing Wang, Hui Liu, Xiaohui Guo	Specify and Compose Web Services by TLA.	ICWS	2008	DBLP DOI BibTeX RDF
36	Hocine El-Habib Daho, Djilali Benhamamouch	Formal Verification of ASM Models Using TLA+.	ABZ	2008	DBLP DOI BibTeX RDF
36	Gudmund Grov, Greg Michaelson, Andrew Ireland	Formal verification of concurrent scheduling strategies using TLA.	ICPADS	2007	DBLP DOI BibTeX RDF
36	Nicolas Rivierre, François Horn, Frédéric Dang Tran	On Monitoring Concurrent Systems with TLA: An Example.	ACSD	2005	DBLP DOI BibTeX RDF
36	Yifeng Chen, Zhiming Liu 0001	From Durational Specifications to TLA Designs of Timed Automata.	ICFEM	2004	DBLP DOI BibTeX RDF
36	Leslie Lamport, John Matthews, Mark R. Tuttle, Yuan Yu	Specifying and verifying systems with TLA+.	ACM SIGOPS European Workshop	2002	DBLP DOI BibTeX RDF
36	Stephan Merz	A More Complete TLA.	World Congress on Formal Methods	1999	DBLP DOI BibTeX RDF
36	Leslie Lamport	TLA in Pictures.	IEEE Trans. Software Eng.	1995	DBLP DOI BibTeX RDF	Concurrency, specification, temporal logic, state-transition diagrams
36	Sara Kalvala	A Formulation of TLA in Isabelle.	TPHOLs	1995	DBLP DOI BibTeX RDF
36	Urban Engberg, Peter Grønning, Leslie Lamport	Mechanical Verification of Concurrent Systems with TLA.	CAV	1992	DBLP DOI BibTeX RDF
30	Leslie Lamport	The PlusCal Algorithm Language.	ICTAC	2009	DBLP DOI BibTeX RDF
30	Yuko Sakurai, Yasumasa Saito, Atsushi Iwasaki, Makoto Yokoo	Sequential partition mechanism for strongly budget-balanced redistribution.	AAMAS (2)	2009	DBLP BibTeX RDF	budget-balance, strategy-proofness, mechanism design, redistribution
30	Robert Palmer, Michael Delisi, Ganesh Gopalakrishnan, Robert M. Kirby	An Approach to Formalization and Analysis of Message Passing Libraries.	FMICS	2007	DBLP DOI BibTeX RDF
30	Asad Awan, Ahmed H. Sameh, Suresh Jagannathan, Ananth Grama	Building Verifiable Sensing Applications Through Temporal Logic Specification.	International Conference on Computational Science (1)	2007	DBLP DOI BibTeX RDF
30	Leslie Lamport	The +CAL Algorithm Language.	NCA	2006	DBLP DOI BibTeX RDF
30	Philippe Collet, Alain Ozanne, Nicolas Rivierre	Enforcing Different Contracts in Hierarchical Component-Based Systems.	SC@ETAPS	2006	DBLP DOI BibTeX RDF
30	Leslie Lamport	The +CAL Algorithm Language.	FORTE	2006	DBLP DOI BibTeX RDF
30	Adrianna Alexander, Wolfgang Reisig	Logic of Involved Variables - System Specification with Temporal Logic of Distributed Actions.	ACSD	2003	DBLP DOI BibTeX RDF
30	Ulka Shrotri, Purandar Bhaduri, R. Venkatesh 0001	Model Checking Visual Specification of Requirements.	SEFM	2003	DBLP DOI BibTeX RDF
30	Yuguang Fang	General Modeling and Performance Analysis for Location Management in Wireless Mobile Networks.	IEEE Trans. Computers	2002	DBLP DOI BibTeX RDF	pointer forwarding, two-location algorithm, wireless networks, mobile networks, Mobility management, location management, cost analysis
30	Joseph E. Stoy, Xiaowei Shen, Arvind	Proofs of Correctness of Cache-Coherence Protocols.	FME	2001	DBLP DOI BibTeX RDF
30	Holger Busch	A Practical Method for Reasoning about Distributed Systems in a Theorem Prover.	TPHOLs	1995	DBLP DOI BibTeX RDF
30	Thomas Långbacka	A HOL Formalisation of the Temporal Logic of Actions.	TPHOLs	1994	DBLP DOI BibTeX RDF
30	Limor Fix, Fred B. Schneider	Reasoning about Programs by Exploiting the Environment.	ICALP	1994	DBLP DOI BibTeX RDF
30	Shengzong Zhou, Rob Gerth, Ruurd Kuiper 0001	Transformations Preserving Properties and Properties Preserved by Transformations in Fair Transition Systems (Extended Abstract).	CONCUR	1993	DBLP DOI BibTeX RDF
23	Robert Beers	Pre-RTL formal verification: an intel experience.	DAC	2008	DBLP DOI BibTeX RDF	TLC, explicit state enumeration, microarchitecture verification, formal verification, protocol verification, TLA+
23	Philippe Collet, Alain Ozanne, Nicolas Rivierre	On contracting different behavioral properties in component-based systems.	SAC	2006	DBLP DOI BibTeX RDF	verification, component, contract, assertion, TLA
23	Leslie Lamport	Verification and Specifications of Concurrent Programs.	REX School/Symposium	1993	DBLP DOI BibTeX RDF	Assertional methods, Owicki-Gries method, formal methods, temporal logic, fairness, mathematics, TLA
21	Peng Gao, Chun-Lin Ji, Tao Yu, Ru-Yue Yuan	YOLO-TLA: An Efficient and Lightweight Small Object Detection Model based on YOLOv5.	CoRR	2024	DBLP DOI BibTeX RDF
21	José E. Solsona	On the specification and verification of the PCR parallel programming pattern in TLA+.	CLEI Electron. J.	2023	DBLP DOI BibTeX RDF
21	Tatjana Kapus	Improved Formal Verification of SDN-Based Firewalls by Using TLA+.	IEEE Access	2023	DBLP DOI BibTeX RDF
21	Paolo Dini, Manuel Bravo, Philipp Paulweber, Alexander Raschke, Gabriela Moreira	Tutorial on the Executable ASM Specification of the AB Protocol and Comparison with TLA+.	CoRR	2023	DBLP DOI BibTeX RDF
21	Lingzhi Ouyang, Yu Huang 0002, Binyu Huang, Hengfeng Wei, Xiaoxing Ma	Leveraging TLA+ Specifications to Improve the Reliability of the ZooKeeper Coordination Service.	CoRR	2023	DBLP DOI BibTeX RDF
21	Matthias Grundmann, Hannes Hartenstein	Towards a Formal Verification of the Lightning Network with TLA+.	CoRR	2023	DBLP DOI BibTeX RDF
21	Markus A. Kuppe	Teaching TLA+ to Engineers at Microsoft.	FMTea	2023	DBLP DOI BibTeX RDF
21	Rodrigo Otoni, Igor Konnov 0001, Jure Kukovec, Patrick Eugster, Natasha Sharygina	Symbolic Model Checking for TLA+ Made Faster.	TACAS (1)	2023	DBLP DOI BibTeX RDF
21	Lingzhi Ouyang, Yu Huang 0002, Binyu Huang, Xiaoxing Ma	Leveraging TLA+ Specifications to Improve the Reliability of the ZooKeeperCoordination Service.	SETTA	2023	DBLP DOI BibTeX RDF
21	A. Finn Hackett, Joshua Rowe, Markus Alexander Kuppe	Understanding Inconsistency in Azure Cosmos DB with TLA+.	ICSE-SEIP	2023	DBLP DOI BibTeX RDF
21	A. Finn Hackett, Joshua Rowe, Markus Alexander Kuppe	Understanding Inconsistency in Azure Cosmos DB with TLA+.	CoRR	2022	DBLP DOI BibTeX RDF
21	Igor Konnov 0001, Markus Kuppe, Stephan Merz	Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS.	CoRR	2022	DBLP DOI BibTeX RDF
21	Xiaosong Gu, Wei Cao, Yicong Zhu, Xuan Song, Yu Huang 0002, Xiaoxing Ma	Compositional Model Checking of Consensus Protocols Specified in TLA+ via Interaction-Preserving Abstraction.	CoRR	2022	DBLP BibTeX RDF
21	William Schultz, Ian Dardik, Stavros Tripakis	Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+.	CoRR	2022	DBLP DOI BibTeX RDF
21	Matthias Grundmann, Hannes Hartenstein	Verifying Payment Channels with TLA+.	ICBC	2022	DBLP DOI BibTeX RDF
21	Igor Konnov 0001, Markus Kuppe, Stephan Merz	Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS.	ISoLA (1)	2022	DBLP DOI BibTeX RDF
21	Zeinab Nehaï, François Bobot, Sara Tucci Piergiovanni, Carole Delporte-Gallet, Hugues Fauconnier	A TLA+ Formal Proof of a Cross-Chain Swap.	ICDCN	2022	DBLP DOI BibTeX RDF
21	Gabriela Moreira, Cristiano D. Vasconcellos, Janine Kniess	Fully-Tested code generation from TLA+ specifications.	SAST	2022	DBLP DOI BibTeX RDF
21	Ryo Matsumoto, Shenghong Ye, Yuya Mikami, Kazutoshi Kato	Model Development for Fast Wavelength Switching at Tunable DFB Laser Array (TLA).	OECC/PSC	2022	DBLP DOI BibTeX RDF
21	Madhusmita Das, Biju R. Mohan, Ram Mohana Reddy Guddeti	Formal Specification and Verification of Drone System using TLA+: A Case Study.	SNPD	2022	DBLP DOI BibTeX RDF
21	William Schultz, Ian Dardik, Stavros Tripakis	Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+.	FMCAD	2022	DBLP DOI BibTeX RDF
21	Gasper Petelin, Gjorgjina Cenikj, Tome Eftimov	TLA: Topological Landscape Analysis for Single-Objective Continuous Optimization Problem Instances.	SSCI	2022	DBLP DOI BibTeX RDF
21	Luming Dong, Zhi Niu, Yong Zhu, Wei Zhang	Specifying and Verifying SDP Protocol Based Zero Trust Architecture Using TLA+.	ICCSIE	2022	DBLP DOI BibTeX RDF
21	Zhi Niu, Luming Dong, Yong Zhu, Li Chen	Verifying Zookeeper based on Model-Based runtime Trace-Checking using TLA+.	ICCSIE	2022	DBLP DOI BibTeX RDF
21	Markus Alexander Kuppe	The TLA+ Debugger.	SEFM Workshops	2022	DBLP DOI BibTeX RDF
21	Christos Grompanopoulos, Antonios Gouglidis, Anastasia Mavridou	Specifying and verifying usage control models and policies in TLA+.	Int. J. Softw. Tools Technol. Transf.	2021	DBLP DOI BibTeX RDF
21	Tushar Sarkar, Nishant Rajadhyaksha	TLA: Twitter Linguistic Analysis.	CoRR	2021	DBLP BibTeX RDF
21	Smruti Padhy, Joe Stubbs	Designing and Proving Properties of the Abaco Autoscaler Using TLA+.	VSTTE	2021	DBLP DOI BibTeX RDF
21	Nawar H. Obeidat, Carla Purdy	Improving Security in SCADA Systems through Model-checking with TLA+.	MWSCAS	2021	DBLP DOI BibTeX RDF
21	Brent Smith, Laura Milham	Total Learning Architecture (TLA) Data Pillars and Their Applicability to Adaptive Instructional Systems.	HCI (42)	2021	DBLP DOI BibTeX RDF
21	Leslie Lamport, Fred B. Schneider	Verifying Hyperproperties With TLA.	CSF	2021	DBLP DOI BibTeX RDF
21	Young-Mi Kim, Miyoung Kang	Formal Verification of SDN-Based Firewalls by Using TLA+.	IEEE Access	2020	DBLP DOI BibTeX RDF
21	Jiaqi Yin, Huibiao Zhu, Yuan Fei	Specification and Verification of the Zab Protocol with TLA+.	J. Comput. Sci. Technol.	2020	DBLP DOI BibTeX RDF
21	Gefei Zhang	Specifying and Model Checking Workflows of Single Page Applications with TLA+.	CoRR	2020	DBLP BibTeX RDF
21	Sangwon Seo, Sangbae Yun, Jaehong Kim 0006, Inkyo Kim, Seongwook Jin, Seungryoul Maeng	H-TLA: Hybrid-Based and Two-Level Addressing Architecture for IoT Devices and Services.	IEICE Trans. Inf. Syst.	2020	DBLP DOI BibTeX RDF
21	Tatjana Kapus	Specifying reversibility with TLA+.	J. Log. Algebraic Methods Program.	2020	DBLP DOI BibTeX RDF
21	Michael J. Butler, Alexander Raschke	Abstract State Machines, Alloy, B, TLA, VDM and Z (ABZ 2018).	Sci. Comput. Program.	2020	DBLP DOI BibTeX RDF