Bengt Jonsson

SL^λ: A Scalable Algorithm for Register Automata Learning

Dierl, Simon; Fiterău-Broştean, Paul; Howar, Falk; Jonsson, Bengt et al.

Part of Journal of automated reasoning, 2026

• DOI for SL^λ: A Scalable Algorithm for Register Automata Learning
• Download full text (pdf) of SL^λ: A Scalable Algorithm for Register Automata Learning

Efficient Linearizability Monitoring

Abdulla, Parosh; Grahn, Samuel; Jonsson, Bengt; Krishna, Shankaranarayanan et al.

Part of Proceedings of the ACM on Programming Languages, p. 1937-1960, 2025

• DOI for Efficient Linearizability Monitoring
• Download full text (pdf) of Efficient Linearizability Monitoring

Awaiting for Godot: stateless model checking that avoids executions where nothing happens

Jonsson, Bengt; Lång, Magnus; Sagonas, Konstantinos

Part of Formal methods in system design, p. 71-105, 2025

• DOI for Awaiting for Godot: stateless model checking that avoids executions where nothing happens
• Download full text (pdf) of Awaiting for Godot: stateless model checking that avoids executions where nothing happens

Timing is All You Need

Graf, Susanne; Jonsson, Bengt; Khodabandeloo, Behnam; Huang, Chengzi et al.

Part of The Combined Power of Research, Education, and Dissemination, p. 259-279, Springer, 2025

• DOI for Timing is All You Need

Parsimonious Optimal Dynamic Partial Order Reduction

Abdulla, Parosh; Atig, Mohamed Faouzi; Das, Sarbojit; Jonsson, Bengt et al.

Part of Computer Aided Verification, PT II, CAV 2024, p. 19-43, 2024

• DOI for Parsimonious Optimal Dynamic Partial Order Reduction
• Download full text (pdf) of Parsimonious Optimal Dynamic Partial Order Reduction

SL^λ: A Scalable Algorithm for Register Automata Learning

Dierl, Simon; Fiterău-Broştean, Paul; Howar, Falk; Jonsson, Bengt et al.

Part of Journal of automated reasoning, 2026

• DOI for SL^λ: A Scalable Algorithm for Register Automata Learning
• Download full text (pdf) of SL^λ: A Scalable Algorithm for Register Automata Learning

Efficient Linearizability Monitoring

Abdulla, Parosh; Grahn, Samuel; Jonsson, Bengt; Krishna, Shankaranarayanan et al.

Part of Proceedings of the ACM on Programming Languages, p. 1937-1960, 2025

• DOI for Efficient Linearizability Monitoring
• Download full text (pdf) of Efficient Linearizability Monitoring

Awaiting for Godot: stateless model checking that avoids executions where nothing happens

Jonsson, Bengt; Lång, Magnus; Sagonas, Konstantinos

Part of Formal methods in system design, p. 71-105, 2025

• DOI for Awaiting for Godot: stateless model checking that avoids executions where nothing happens
• Download full text (pdf) of Awaiting for Godot: stateless model checking that avoids executions where nothing happens

Lock-free Contention Adapting Search Trees

Winblad, Kjell; Sagonas, Konstantinos; Jonsson, Bengt

Part of ACM TRANSACTIONS ON PARALLEL COMPUTING, 2021

• DOI for Lock-free Contention Adapting Search Trees

Optimal stateless model checking for reads-from equivalence under sequential consistency

Abdulla, Parosh; Atig, Mohamed Faouzi; Jonsson, Bengt; Lång, Magnus et al.

Part of Proceedings of the ACM on Programming Languages, p. 1-29, 2019

• DOI for Optimal stateless model checking for reads-from equivalence under sequential consistency
• Download full text (pdf) of Optimal stateless model checking for reads-from equivalence under sequential consistency

Exposing inter-process information for efficient PDES of spatial stochastic systems on multicores

Lindén, Jonatan; Bauer, Pavol; Engblom, Stefan; Jonsson, Bengt

Part of ACM Transactions on Modeling and Computer Simulation, 2019

• DOI for Exposing inter-process information for efficient PDES of spatial stochastic systems on multicores

Optimal Stateless Model Checking under the Release-Acquire Semantics

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Jonsson, Bengt; Ngo, Tuan-Phong

Part of Proceedings of the ACM on Programming Languages, p. 1-29, 2018

• DOI for Optimal Stateless Model Checking under the Release-Acquire Semantics
• Download full text (pdf) of Optimal Stateless Model Checking under the Release-Acquire Semantics

An integrated specification and verification technique for highly concurrent data structures for highly concurrent data structures

Abdulla, Parosh; Haziza, Frédéric; Holík, Lukás; Jonsson, Bengt et al.

Part of International Journal on Software Tools for Technology Transfer, p. 549-563, 2017

• DOI for An integrated specification and verification technique for highly concurrent data structures for highly concurrent data structures

Stateless model checking for TSO and PSO

Abdulla, Parosh Aziz; Aronis, Stavros; Atig, Mohamed Faouzi; Jonsson, Bengt et al.

Part of Acta Informatica, p. 789-818, 2017

• DOI for Stateless model checking for TSO and PSO

Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction

Abdulla, Parosh; Aronis, Stavros; Jonsson, Bengt; Sagonas, Konstantinos

Part of Journal of the ACM, 2017

• DOI for Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction

Verification of heap manipulating programs with ordered data by extended forest automata

Abdulla, Parosh Aziz; Holík, Lukás; Jonsson, Bengt; Lengál, Ondrej et al.

Part of Acta Informatica, p. 357-385, 2016

• DOI for Verification of heap manipulating programs with ordered data by extended forest automata

Active learning for extended finite state machines

Cassel, Sofia; Howar, Falk; Jonsson, Bengt; Steffen, Bernhard

Part of Formal Aspects of Computing, p. 233-263, 2016

• DOI for Active learning for extended finite state machines

A succinct canonical register automaton model

Cassel, Sofia; Howar, Falk; Jonsson, Bengt; Merten, Maik et al.

Part of Journal of Logical and Algebraic Methods in Programming, p. 54-66, 2015

• DOI for A succinct canonical register automaton model

Generating models of infinite-state communication protocols using regular inference with abstraction

Aarts, Fides; Jonsson, Bengt; Uijen, Johan; Vaandrager, Frits

Part of Formal methods in system design, p. 1-41, 2015

• DOI for Generating models of infinite-state communication protocols using regular inference with abstraction

Compositional assume–guarantee reasoning for input/output component theories

Chilton, Chris; Jonsson, Bengt; Kwiatkowska, Marta

Part of Science of Computer Programming, p. 115-137, 2014

• DOI for Compositional assume–guarantee reasoning for input/output component theories

An algebraic theory of interface automata

Chilton, Chris; Jonsson, Bengt; Kwiatkowska, Marta

Part of Theoretical Computer Science, p. 146-174, 2014

• DOI for An algebraic theory of interface automata

Building timing predictable embedded systems

Axer, Philip; Ernst, Rolf; Falk, Heiko; Girault, Alain et al.

Part of ACM Transactions on Embedded Computing Systems, 2014

• DOI for Building timing predictable embedded systems

Regular model checking for LTL(MSO)

Abdulla, Parosh; Jonsson, Bengt; Nilsson, Marcus; d'Orso, Julien et al.

Part of International Journal on Software Tools for Technology Transfer, p. 223-241, 2012

• DOI for Regular model checking for LTL(MSO)

Using refinement calculus techniques to prove linearizability

Jonsson, Bengt

Part of Formal Aspects of Computing, p. 537-554, 2012

• DOI for Using refinement calculus techniques to prove linearizability

Learning of event-recording automata

Grinchtein, Olga; Jonsson, Bengt; Leucker, Martin

Part of Theoretical Computer Science, p. 4029-4054, 2010

• DOI for Learning of event-recording automata

State-space exploration for concurrent algorithms under weak memory orderings

Jonsson, Bengt

Part of SIGARCH Computer Architecture News, p. 65-71, 2008

• DOI for State-space exploration for concurrent algorithms under weak memory orderings

Simulating perfect channels with probabilistic lossy channels

Abdulla, Parosh; Baier, Christel; Iyer, S. Purushotaman; Jonsson, Bengt

Part of Information and Computation, p. 22-40, 2005

Insights to Angluin's Learning

Berg, Therese; Jonsson, Bengt; Leucker, Martin; Saksena, Mayank

Part of Electr. Notes on Theoret. Comput. Sci., p. 3-18, 2005

Using Forward Reachability Analysis for Verification of Lossy Channel Systems

Abdulla, Parosh Aziz; Collomb-Annichini, Aurore; Bouajjani, Ahmed; Jonsson, Bengt

Part of Formal methods in system design, p. 39-65, 2004

• DOI for Using Forward Reachability Analysis for Verification of Lossy Channel Systems

Model checking of systems with many identical timed processes

Abdulla, Parosh; Jonsson, Bengt

Part of Theoretical Computer Science, p. 241-264, 2003

• DOI for Model checking of systems with many identical timed processes

ASTEC: An Experience in the Establishment of Collaboration between Academia and Industry

Jonsson, Bengt; Sagonas, Konstantinos

Part of Springer International Journal on Software Tools for Technology Transfer, p. 401-404, 2003

Testing preorders for probabilistic processes can be characterized by simulations

Jonsson, Bengt; Yi, Wang

Part of Theoretical Computer Science, p. 33-51, 2002

Algorithmic analysis of programs with well quasi-ordered domains

Abdulla, PA; Cerans, K; Jonsson, B; Tsay, YK

Part of INFORMATION AND COMPUTATION, p. 109-127, 2000

Proving Refinement Using Transduction

Jonsson, Bengt; Pnueli, Amir; Rump, Camilla

Part of Distributed Computing, p. 129-150, 1999

Verifying programs with unreliable channels

Abdulla, PA; Jonsson, B

Part of Information and Computation, p. 91-101, 1996

• DOI for Verifying programs with unreliable channels

Deciding Bisimulation Equivalences for a Class of Non-Finite-State Programs

Jonsson, Bengt; Parrow, Joachim

Part of Information and Computation, p. 272-302, 1993

• DOI for Deciding Bisimulation Equivalences for a Class of Non-Finite-State Programs

Timing is All You Need

Graf, Susanne; Jonsson, Bengt; Khodabandeloo, Behnam; Huang, Chengzi et al.

Part of The Combined Power of Research, Education, and Dissemination, p. 259-279, Springer, 2025

• DOI for Timing is All You Need

Trading Space for Simplicity in Stateless Model Checking

Abdulla, Parosh; Atig, Mohamed Faouzi; Das, Sarbojit; Jonsson, Bengt et al.

Part of Real Time and Such, p. 79-97, Springer, 2024

• DOI for Trading Space for Simplicity in Stateless Model Checking

Consistency and Persistency in Program Verification: Challenges and Opportunities

Abdulla, Parosh; Atig, Mohamed Faouzi; Bouajjani, Ahmed; Jonsson, Bengt et al.

Part of Principles of Systems Design, p. 494-510, Springer, 2022

• DOI for Consistency and Persistency in Program Verification: Challenges and Opportunities

Comparing source sets and persistent sets for partial order reduction

Abdulla, Parosh; Aronis, Stavros; Jonsson, Bengt; Sagonas, Konstantinos

Part of Models, Algorithms, Logics and Tools, p. 516-536, Springer, 2017

• DOI for Comparing source sets and persistent sets for partial order reduction

Learning of automata models extended with data

Jonsson, Bengt

Part of Formal Methods for Eternal Networked Software Systems, p. 327-349, Springer Berlin/Heidelberg, 2011

• DOI for Learning of automata models extended with data

Probabilistic Extensions of Process Algebras

Jonsson, Bengt; Larsen, Kim; Yi, Wang

p. 685-710, ELSEVIER, 2001

On the existence of network invariants for verifying parameterized systems

Abdulla, Parosh; Jonsson, Bengt

Part of Correct System Design, p. 180-197, Springer-Verlag, Berlin, 1999

Parsimonious Optimal Dynamic Partial Order Reduction

Abdulla, Parosh; Atig, Mohamed Faouzi; Das, Sarbojit; Jonsson, Bengt et al.

Part of Computer Aided Verification, PT II, CAV 2024, p. 19-43, 2024

• DOI for Parsimonious Optimal Dynamic Partial Order Reduction
• Download full text (pdf) of Parsimonious Optimal Dynamic Partial Order Reduction

Monitor-based Testing of Network Protocol Implementations Using Symbolic Execution

Asadian, Hooman; Fiterau-Brostean, Paul; Jonsson, Bengt; Sagonas, Konstantinos

Part of 19TH INTERNATIONAL CONFERENCE ON AVAILABILITY, RELIABILITY, AND SECURITY, ARES 2024, 2024

• DOI for Monitor-based Testing of Network Protocol Implementations Using Symbolic Execution

Testing IoT Protocol Requirements Using Fuzzing and Symbolic Execution: Application to CoAP

Asadian, Hooman; Fiterău-Broştean, Paul; Jonsson, Bengt; Sagonas, Konstantinos

Part of 2024 IEEE Conference on Standards for Communications and Networking (CSCN), p. 48-54, 2024

• DOI for Testing IoT Protocol Requirements Using Fuzzing and Symbolic Execution: Application to CoAP

Parsimonious Optimal Dynamic Partial Order Reduction

Abdulla, Parosh; Atig, Mohamed Faouzi; Das, Sarbojit; Jonsson, Bengt et al.

2024

• Download full text (pdf) of Parsimonious Optimal Dynamic Partial Order Reduction

SMBugFinder: An Automated Framework for Testing Protocol Implementations for State Machine Bugs

Fiterau-Brostean, Paul; Jonsson, Bengt; Sagonas, Konstantinos; Tåquist, Fredrik

Part of PROCEEDINGS OF THE 33RD ACM SIGSOFT INTERNATIONAL SYMPOSIUM ON SOFTWARE TESTING AND ANALYSIS, ISSTA 2024, p. 1866-1870, 2024

• DOI for SMBugFinder: An Automated Framework for Testing Protocol Implementations for State Machine Bugs

Scalable Tree-based Register Automata Learning

Dierl, Simon; Fiterau-Brostean, Paul; Howar, Falk; Jonsson, Bengt et al.

Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 87-108, 2024

• DOI for Scalable Tree-based Register Automata Learning
• Download full text (pdf) of Scalable Tree-based Register Automata Learning

Automata-Based Automated Detection of State Machine Bugs in Protocol Implementations

Fiterau-Brostean, Paul; Jonsson, Bengt; Sagonas, Konstantinos; Tåquist, Fredrik

Part of Network and Distributed System Security (NDSS) Symposium 2023, p. 1-18, 2023

• DOI for Automata-Based Automated Detection of State Machine Bugs in Protocol Implementations

CONCUR Test-Of-Time Award 2023

Jonsson, Bengt; Kwiatkowska, Marta; Walukiewicz, Igor

Part of 34th International Conference on Concurrency Theory (CONCUR 2023), 2023

• DOI for CONCUR Test-Of-Time Award 2023
• Download full text (pdf) of CONCUR Test-Of-Time Award 2023

Tailoring Stateless Model Checking for Event-Driven Multi-threaded Programs

Abdulla, Parosh; Atig, Mohamed Faouzi; Meyer Bønneland, Frederik; Das, Sarbojit et al.

Part of Automated Technology for Verification and Analysis, p. 176-198, 2023

• DOI for Tailoring Stateless Model Checking for Event-Driven Multi-threaded Programs
• Download full text (pdf) of Tailoring Stateless Model Checking for Event-Driven Multi-threaded Programs

An Active Learning Approach to Synthesizing Program Contracts

Ghosal, Sandip; Jonsson, Bengt; Rümmer, Philipp

Part of Software Engineering and Formal Methods, SEFM 2023, p. 126-144, 2023

• DOI for An Active Learning Approach to Synthesizing Program Contracts

An Active Learning Approach to Synthesizing Program Contracts

Ghosal, Sandip; Jonsson, Bengt; Rümmer, Philipp

2023

Applying Symbolic Execution to Test Implementations of a Network Protocol Against its Specification

Asadian, Hooman; Fiterau-Brostean, Paul; Jonsson, Bengt; Sagonas, Konstantinos

Part of 2022 IEEE 15TH INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION (ICST 2022), p. 70-81, 2022

• DOI for Applying Symbolic Execution to Test Implementations of a Network Protocol Against its Specification

Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens

Jonsson, Bengt; Lång, Magnus; Sagonas, Konstantinos

Part of 2022 Formal Methods in Computer-Aided Design (FMCAD), p. 284-293, 2022

• DOI for Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens
• Download full text (pdf) of Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens

DTLS-Fuzzer: A DTLS Protocol State Fuzzer

Fiterau-Brostean, Paul; Jonsson, Bengt; Sagonas, Konstantinos; Tåquist, Fredrik

Part of 2022 IEEE 15th International Conference on Software Testing, Verification and Validation (ICST 2022), p. 456-458, 2022

• DOI for DTLS-Fuzzer: A DTLS Protocol State Fuzzer

Analysis of DTLS Implementations Using Protocol State Fuzzing

Fiterau-Brostean, Paul; Jonsson, Bengt; Merget, Robert; de Ruiter, Joeri et al.

Part of Proceedings of the 29th USENIX Security Symposium, p. 2523-2540, 2020

• Download full text (pdf) of Analysis of DTLS Implementations Using Protocol State Fuzzing

Dynamic Partial Order Reduction Under the Release-Acquire Semantics (Tutorial)

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Jonsson, Bengt; Ngo, Tuan-Phong

Part of Networked Systems, p. 3-18, 2019

• DOI for Dynamic Partial Order Reduction Under the Release-Acquire Semantics (Tutorial)

Optimal dynamic partial order reduction with observers

Aronis, Stavros; Jonsson, Bengt; Lång, Magnus; Sagonas, Konstantinos

Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 229-248, 2018

• DOI for Optimal dynamic partial order reduction with observers
• Download full text (pdf) of Optimal dynamic partial order reduction with observers

Optimal Stateless Model Checking under the Release-Acquire Semantics

Abdulla, Parosh; Atig, Mohamed Faouzi; Jonsson, Bengt; Ngo, Tuan-Phong

Part of SPLASH OOPSLA 2018, Boston, Nov 4-9, 2018, 2018

• DOI for Optimal Stateless Model Checking under the Release-Acquire Semantics

Fragment abstraction for concurrent shape analysis

Abdulla, Parosh Aziz; Jonsson, Bengt; Trinh, Cong Quy

Part of Programming Languages and Systems, p. 442-471, 2018

• DOI for Fragment abstraction for concurrent shape analysis

Lock-free Contention Adapting Search Trees

Winblad, Kjell; Sagonas, Konstantinos; Jonsson, Bengt

Part of The 30th ACM Symposium on Parallelism in Algorithms and Architectures, SPAA 2018, 2018

• DOI for Lock-free Contention Adapting Search Trees

Fine-grained local dynamic load balancing in PDES

Lindén, Jonatan; Bauer, Pavol; Engblom, Stefan; Jonsson, Bengt

Part of Proc. 6th ACM SIGSIM Conference on Principles of Advanced Discrete Simulation, p. 201-212, 2018

• DOI for Fine-grained local dynamic load balancing in PDES

The Quest for Optimality in Stateless Model Checking of Concurrent Programs

Jonsson, Bengt

Part of Formal Methods For Industrial Critical Systems, FMICS 2018, 2018

Extending Automata Learning to Extended Finite State Machines

Cassel, Sofia; Howar, Falk; Jonsson, Bengt; Steffen, Bernhard

Part of Machine Learning for Dynamic Software Analysis, p. 149-177, 2018

• DOI for Extending Automata Learning to Extended Finite State Machines

Exposing inter-process information for efficient parallel discrete event simulation of spatial stochastic systems

Lindén, Jonatan; Bauer, Pavol; Engblom, Stefan; Jonsson, Bengt

Part of Proc. 5th ACM SIGSIM Conference on Principles of Advanced Discrete Simulation, p. 53-64, 2017

• DOI for Exposing inter-process information for efficient parallel discrete event simulation of spatial stochastic systems

Automated Verification of Linearization Policies

Abdulla, Parosh; Jonsson, Bengt; Trinh, Cong Quy

Part of Automated Verification of Linearization Policies, 2016

• DOI for Automated Verification of Linearization Policies

Stateless model checking for POWER

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Jonsson, Bengt; Leonardsson, Carl

Part of Computer Aided Verification, p. 134-156, 2016

• DOI for Stateless model checking for POWER

Industrial Evaluation of Test Suite Generation Strategies for Model-Based Testing

Blom, Johan; Jonsson, Bengt; Nyström, Sven-Olof

2016

• DOI for Industrial Evaluation of Test Suite Generation Strategies for Model-Based Testing

Efficient inter-process synchronization for parallel discrete event simulation on multicores

Bauer, Pavol; Lindén, Jonatan; Engblom, Stefan; Jonsson, Bengt

Part of Proc. 3rd ACM SIGSIM Conference on Principles of Advanced Discrete Simulation, p. 183-194, 2015

• DOI for Efficient inter-process synchronization for parallel discrete event simulation on multicores

Stateless model checking for TSO and PSO

Abdulla, Parosh Aziz; Aronis, Stavros; Atig, Mohamed Faouzi; Jonsson, Bengt et al.

Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 353-367, 2015

• DOI for Stateless model checking for TSO and PSO

RALib: A LearnLib extension for inferring EFSMs

Cassel, Sofia; Falk, Howar; Jonsson, Bengt

2015

Mediator synthesis in a component algebra with data

Holik, Lukás; Isberner, Malte; Jonsson, Bengt

Part of Correct System Design, p. 238-259, 2015

• DOI for Mediator synthesis in a component algebra with data

A Modeling Framework for Reuse Distance-based Estimation of Cache Performance

Pan, Xiaoyue; Jonsson, Bengt

Part of Performance Analysis of Systems and Software (ISPASS), 2015 IEEE International Symposium on, p. 62-71, 2015

• DOI for A Modeling Framework for Reuse Distance-based Estimation of Cache Performance

Learning Extended Finite State Machines

Cassel, Sofia; Howar, Falk; Jonsson, Bengt; Steffen, Bernhard

Part of Software Engineering and Formal Methods.  12th International Conference, SEFM 2014, p. 250-264, 2014

• DOI for Learning Extended Finite State Machines

A constraint programming approach for managing end-to-end requirements in sensor network macroprogramming

Hassani Bijarbooneh, Farshid; Pathak, Animesh; Pearson, Justin; Issarny, Valérie et al.

Part of Proc. 3rd International Conference on Sensor Networks, p. 28-40, 2014

• DOI for A constraint programming approach for managing end-to-end requirements in sensor network macroprogramming

Optimal dynamic partial order reduction

Abdulla, Parosh; Aronis, Stavros; Jonsson, Bengt; Sagonas, Konstantinos

Part of Proc. 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, p. 373-384, 2014

• DOI for Optimal dynamic partial order reduction

Modeling cache coherence misses on multicores

Pan, Xiaoyue; Jonsson, Bengt

Part of 2014 IEEE INTERNATIONAL SYMPOSIUM ON PERFORMANCE ANALYSIS OF SYSTEMS AND SOFTWARE (ISPASS), p. 96-105, 2014

• DOI for Modeling cache coherence misses on multicores

An Integrated Specification and Verification Technique for Highly Concurrent Data Structures

Abdulla, Parosh Aziz; Haziza, Frédéric; Holik, Lukas; Jonsson, Bengt et al.

Part of Tools and Algorithms for the Construction and Analysis of Systems, 2013

• Download full text (pdf) of An Integrated Specification and Verification Technique for Highly Concurrent Data Structures

Verification of heap manipulating programs with ordered data by extended forest automata

Abdulla, Parosh Aziz; Holík, Lukás; Jonsson, Bengt; Lengál, Ondrej et al.

Part of Automated Technology for Verification and Analysis, p. 224-239, 2013

• DOI for Verification of heap manipulating programs with ordered data by extended forest automata
• Download full text (pdf) of Verification of heap manipulating programs with ordered data by extended forest automata

A Skiplist-based Concurrent Priority Queue with Minimal Memory Contention

Lindén, Jonatan; Jonsson, Bengt

Part of OPODIS 2013: 17th International Conference On Principles Of DIstributed Systems, p. 206-220, 2013

• DOI for A Skiplist-based Concurrent Priority Queue with Minimal Memory Contention

Automated Mediator Synthesis: Combining Behavioural and Ontological Reasoning

Benaceur, Amel; Chilton, Chris; Isberner, Malte; Jonsson, Bengt

Part of SEFM 2013, 11th Int. Conf. on Software Engineering and Formal Methods, p. 274-288, 2013

• DOI for Automated Mediator Synthesis: Combining Behavioural and Ontological Reasoning

Assume-guarantee reasoning for safe component behaviours

Chilton, C.; Jonsson, Bengt; Kwiatkowska, M.

Part of Formal Aspects of Component Software, p. 92-109, 2013

• DOI for Assume-guarantee reasoning for safe component behaviours

Inferring Canonical Register Automata

Howar, Falk; Steffen, Bernhard; Jonsson, Bengt; Cassel, Sofia

Part of Verification, Model Checking, and Abstract Interpretation - 13th International Conference,, p. 251-266, 2012

• DOI for Inferring Canonical Register Automata

Demonstrating Learning of Register Automata

Merten, Maik; Howar, Falk; Steffen, Bernhard; Cassel, Sofia et al.

Part of Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference,, p. 466-471, 2012

• DOI for Demonstrating Learning of Register Automata

Inferring semantic interfaces of data structures

Howar, F.; Isberner, M.; Steffen, B.; Bauer, O. et al.

Part of Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change, p. 554-571, 2012

• DOI for Inferring semantic interfaces of data structures

A succinct canonical register automaton model for data domains with binary relations

Cassel, Sofia; Jonsson, Bengt; Howar, F.; Steffen, B.

Part of Automated Technology for Verification and Analysis, p. 57-71, 2012

• DOI for A succinct canonical register automaton model for data domains with binary relations

A Compositional Specification Theory for Component Behaviours

Chen, Taolue; Chilton, Chris; Jonsson, Bengt; Kwiatkowska, Marta

Part of Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012,, p. 148-168, 2012

• DOI for A Compositional Specification Theory for Component Behaviours

Predicting the Cost of Lock Contention in Parallel Applications on Multicores using Analytic Modeling

Pan, Xiaoyue; Lindén, Jonatan; Jonsson, Bengt

Part of Proc. 5th Swedish Workshop on Multi-Core Computing, 2012

Assume-Guarantee Reasoning for Safe Component Behaviours

Chilton, Chris; Jonsson, Bengt; Kwiatkowska, Marta

Part of Proc. FACS: Formal Aspects of Component Software, 9th Int. Symp., p. 92-109, 2012

• DOI for Assume-Guarantee Reasoning for Safe Component Behaviours

A succinct canonical register automaton model

Cassel, Sofia; Howar, Falk; Jonsson, Bengt; Merten, Maik et al.

Part of Automated Technology for Verification and Analysis, p. 366-380, 2011

• DOI for A succinct canonical register automaton model

On Handling Data in Automata Learning: Considerations from the CONNECT Perspective

Howar, Falk; Jonsson, Bengt; Merten, Maik; Steffen, Bernhard et al.

Part of Leveraging Applications of Formal Methods, Verification, and Validation, p. 221-235, 2010

• DOI for On Handling Data in Automata Learning: Considerations from the CONNECT Perspective

Inferring Compact Models of Communication Protocol Entities

Bohlin, Therese; Jonsson, Bengt; Soleimanifard, Siavash

Part of Leveraging Applications of Formal Methods, Verification, and Validation, p. 658-672, 2010

• DOI for Inferring Compact Models of Communication Protocol Entities

Generating Models of Infinite-State Communication Protocols Using Regular Inference with Abstraction

Aarts, Fides; Jonsson, Bengt; Uijen, Johan

Part of Testing Software and Systems, p. 188-204, 2010

• DOI for Generating Models of Infinite-State Communication Protocols Using Regular Inference with Abstraction

CONNECT Challenges: Towards Emergent Connectors for Eternal Networked Systems

Issarny, Valérie; Steffen, Bernhard; Jonsson, Bengt; Blair, Gordon et al.

Part of Proc. 14th International Conference on Engineering of Complex Computer Systems, p. 154-161, 2009

• DOI for CONNECT Challenges: Towards Emergent Connectors for Eternal Networked Systems

Using SPIN to model check concurrent algorithms, using a translation from C to Promela

Jiang, Ke; Jonsson, Bengt

Part of Proc. 2nd Swedish Workshop on Multi-Core Computing, p. 67-69, 2009

• Download full text (pdf) of Using SPIN to model check concurrent algorithms, using a translation from C to Promela

Cyclic dependencies in modular performance analysis

Jonsson, Bengt; Perathoner, Simon; Thiele, Lothar; Yi, Wang

Part of Proc. 8th ACM International Conference on Embedded Software, p. 179-188, 2008

• DOI for Cyclic dependencies in modular performance analysis

Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols

Saksena, Mayank; Wibling, Oskar; Jonsson, Bengt

Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 18-32, 2008

• DOI for Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols

Regular Inference for State Machines Using Domains with Equality Tests

Berg, Therese; Jonsson, Bengt; Raffelt, Harald

Part of Fundamental Approaches to Software Engineering, p. 317-331, 2008

• DOI for Regular Inference for State Machines Using Domains with Equality Tests

State-Space Exploration for Concurrent Algorithms under Weak Memory Orderings

Jonsson, Bengt

Part of Proc. 1st Swedish Workshop on Multi-Core Computing, p. 82-88, 2008

Systematic Acceleration in Regular Model Checking

Jonsson, Bengt; Saksena, Mayank

Part of Computer Aided Verification, p. 131-144, 2007

• DOI for Systematic Acceleration in Regular Model Checking

Regular Inference for State Machines with Parameters.

Berg, Therese; Jonsson, Bengt; Raffelt, Harald

Part of Fundamental Approaches to Software Engineering, 9th International Conference, FASE 2006,, p. 107-121, 2006

Proving Liveness by Backwards Reachability

Abdulla, Parosh Aziz; Jonsson, Bengt; Rezine, Ahmed; Saksena, Mayank

2006

Inference of Event-Recording Automata using Timed Decision Trees

Grinchtein, Olga; Jonsson, Bengt; Pettersson, Paul

Part of International Conference on Concurrency Theory, 2006

Specifying and Generating Test Cases Using Observer Automata

Blom, Johan; Hessel, Anders; Jonsson, Bengt; Pettersson, Paul

Part of Formal Approaches to Software Testing, p. 125-139, 2005

• DOI for Specifying and Generating Test Cases Using Observer Automata

On the Correspondence Between Conformance Testing and Regular Inference

Berg, Therese; Grinchtein, Olga; Jonsson, Bengt; Leucker, Martin et al.

Part of FASE 2005, p. 175-189, 2005

Inference of Timed Transition Systems

Grinchtein, Olga; Leucker, Martin; Jonsson, Bengt

Part of Proceedings of the 6th International Workshop on Verification of Infinite-State Systems (INFINITY), 2005

Learning of event-recording automata

Grinchtein, Olga; Jonsson, Bengt; Leucker, Martin

Part of FORMATS/FTRTFT 2004, p. 379-396, 2004

• DOI for Learning of event-recording automata

Specifying and Generating Test Cases Using Observer Automata

Blom, Johan; Hessel, Anders; Jonsson, Bengt; Pettersson, Paul

Part of Proceedings of the 4th International Workshop on Formal Approaches to Testing of Software, p. 125-139, 2004

• DOI for Specifying and Generating Test Cases Using Observer Automata

Regular Model Checking for LTL(MSO)

Abdulla, Parosh; Jonsson, Bengt; Nilsson, Marcus; d'Orso, Julien et al.

Part of Computer Aided Verification, p. 348-360, 2004

A Survey of Regular Model Checking.

Abdulla, Parosh; Jonsson, Bengt; Nilsson, Marcus; Saksena, Mayank

Part of CONCUR 2004 - Concurrency Theory, p. 35-48, 2004

Report on Dataflow Dependencies in Billing Processing Systems

Abdulla, Parosh; Ben Henda, Noomene; Deneux, Johann; Jonsson, Bengt et al.

Part of Proc. ISoLA '04: 1st International Symposium on Leveraging Applications of Formal Methods, 2004

Regular Tree Model Checking

Abdulla, Parosh Aziz; Jonsson, Bengt; Mahata, Pritha; d'Orso, Julien

Part of Computer Aided Verification, p. 555-568, 2002

• DOI for Regular Tree Model Checking

Extracting the Process Structure of Erlang Applications

Nyström, J; Jonsson, B

Part of Erlang Workshop, Firenze, Sept. 2, 2002

Extracting the process structure of Erlang applications

Nystrom, Jan; Jonsson, Bengt

Part of Proc. Erlang Workshop, Firenze, Italy, 2001

Regular Model Checking

Bouajjani, A; Jonsson, B; Nilsson, M; Touili, T

Part of Proc. 12th Int. Conf. on Computer Aided Verification, 2000

Fully Abstract Characterization of Probabilistic May Testin

Jonsson, Bengt; Wang, Yi

1999

A general approach to partial order reductions in symbolic verification

Abdulla, Parosh Aziz; Jonsson, Bengt; Kindahl, Mats; Peled, D

Part of Computer Aided Verification, p. 379-390, 1998

• DOI for A general approach to partial order reductions in symbolic verification

Verifying networks of timed processes

Abdulla, Parosh Aziz; Jonsson, Bengt

Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 298-312, 1998

• DOI for Verifying networks of timed processes

Undecidable verification problems for programs with unreliable channels

Abdulla, Parosh Aziz; Jonsson, Bengt

Part of Automata, Languages and Programming, p. 71-90, 1996

• DOI for Undecidable verification problems for programs with unreliable channels

Model-Based Testing of Reactive Systems, Advanced Lectures: outcome of a research seminar

Broy, Manfred; Jonsson, Bengt; Katoen, Joost-Pieter; Leucker, Martin et al.

2005

Uncovering Flaws in Network Protocol Implementations Using Differential Symbolic Execution

Asadian, Hooman; Fiterau-Brostean, Paul; Jonsson, Bengt; Sagonas, Konstantinos

A Skiplist-Based Concurrent Priority Queue with Minimal Memory Contention

Lindén, Jonatan; Jonsson, Bengt

2018

• Download full text (pdf) of A Skiplist-Based Concurrent Priority Queue with Minimal Memory Contention

A Skiplist-Based Concurrent Priority Queue with Minimal Memory Contention

Lindén, Jonatan; Jonsson, Bengt

2018

• Download full text (pdf) of A Skiplist-Based Concurrent Priority Queue with Minimal Memory Contention

Learning Extended Finite State Machines (extended version)

Cassel, Sofia; Howar, Falk; Jonsson, Bengt; Steffen, Bernhard

2015

Active Learning for Extended Finite State Machines

Cassel, Sofia; Howar, Falk; Jonsson, Bengt; Steffen, Bernhard

2015

• Download full text (pdf) of Active Learning for Extended Finite State Machines

Forecasting Lock Contention Before Adopting Another Lock Algorithm

Pan, Xiaoyue; Klaftenegger, David; Jonsson, Bengt

2015

• Download full text (pdf) of Forecasting Lock Contention Before Adopting Another Lock Algorithm

An Algebraic Theory of Interface Automata

Chilton, Chris; Jonsson, Bengt; Kwiatkowska, Marta

2013

A Compositional Specification Theory for Component Behaviours

Chen, Taolue; Chilton, Chris; Jonsson, Bengt; Kwiatkowska, Marta

2012

Learning of Event-Recording Automata

Grinchtein, Olga; Jonsson, Bengt; Leucker, Martin

2008

• Download full text (pdf) of Learning of Event-Recording Automata

Regular Inference for Communication Protocol Entities

Bohlin, Therese; Jonsson, Bengt

2008

• Download full text (pdf) of Regular Inference for Communication Protocol Entities

Inference of Event-Recording Automata using Timed Decision Trees

Grinchtein, Olga; Jonsson, Bengt

2008

• Download full text (pdf) of Inference of Event-Recording Automata using Timed Decision Trees

Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols: (Extended Version)

Saksena, Mayank; Wibling, Oskar; Jonsson, Bengt

2007

Insights to Angluin's Learning

Berg, Therese; Jonsson, Bengt; Leucker, Martin; Saksena, Mayank

2003