Bengt Jonsson
Professor i datorteknik 92 vid Institutionen för informationsteknologi; Datorteknik
- Telefon:
- 018-471 31 57
- Mobiltelefon:
- 070-425 02 40
- E-post:
- Bengt.Jonsson@it.uu.se
- Besöksadress:
- Hus 10, Regementsvägen 10
- Postadress:
- Box 337
751 05 UPPSALA
- Akademiska meriter:
- FD, Docent
Publikationer
Senaste publikationer
Ingår i The Combined Power of Research, Education, and Dissemination, s. 259-279, Springer, 2025
Testing IoT Protocol Requirements Using Fuzzing and Symbolic Execution: Application to CoAP
Ingår i 2024 IEEE Conference on Standards for Communications and Networking (CSCN), s. 48-54, 2024
Parsimonious Optimal Dynamic Partial Order Reduction
2024
Parsimonious Optimal Dynamic Partial Order Reduction
Ingår i COMPUTER AIDED VERIFICATION, PT II, CAV 2024, s. 19-43, 2024
- DOI för Parsimonious Optimal Dynamic Partial Order Reduction
- Ladda ner fulltext (pdf) av Parsimonious Optimal Dynamic Partial Order Reduction
Trading Space for Simplicity in Stateless Model Checking
Ingår i Real Time and Such, s. 79-97, Springer, 2024
Alla publikationer
Artiklar i tidskrift
Lock-free Contention Adapting Search Trees
Ingår i ACM TRANSACTIONS ON PARALLEL COMPUTING, 2021
Optimal stateless model checking for reads-from equivalence under sequential consistency
Ingår i Proceedings of the ACM on Programming Languages, 2019
- DOI för Optimal stateless model checking for reads-from equivalence under sequential consistency
- Ladda ner fulltext (pdf) av Optimal stateless model checking for reads-from equivalence under sequential consistency
Exposing inter-process information for efficient PDES of spatial stochastic systems on multicores
Ingår i ACM Transactions on Modeling and Computer Simulation, 2019
Optimal Stateless Model Checking under the Release-Acquire Semantics
Ingår i Proceedings of the ACM on Programming Languages, s. 1-29, 2018
- DOI för Optimal Stateless Model Checking under the Release-Acquire Semantics
- Ladda ner fulltext (pdf) av Optimal Stateless Model Checking under the Release-Acquire Semantics
Ingår i International Journal on Software Tools for Technology Transfer, s. 549-563, 2017
Stateless model checking for TSO and PSO
Ingår i Acta Informatica, s. 789-818, 2017
Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction
Ingår i Journal of the ACM, 2017
Verification of heap manipulating programs with ordered data by extended forest automata
Ingår i Acta Informatica, s. 357-385, 2016
Active learning for extended finite state machines
Ingår i Formal Aspects of Computing, s. 233-263, 2016
A succinct canonical register automaton model
Ingår i Journal of Logical and Algebraic Methods in Programming, s. 54-66, 2015
Generating models of infinite-state communication protocols using regular inference with abstraction
Ingår i Formal methods in system design, s. 1-41, 2015
Compositional assume–guarantee reasoning for input/output component theories
Ingår i Science of Computer Programming, s. 115-137, 2014
An algebraic theory of interface automata
Ingår i Theoretical Computer Science, s. 146-174, 2014
Building timing predictable embedded systems
Ingår i ACM Transactions on Embedded Computing Systems, 2014
Regular model checking for LTL(MSO)
Ingår i International Journal on Software Tools for Technology Transfer, s. 223-241, 2012
Using refinement calculus techniques to prove linearizability
Ingår i Formal Aspects of Computing, s. 537-554, 2012
Learning of event-recording automata
Ingår i Theoretical Computer Science, s. 4029-4054, 2010
State-space exploration for concurrent algorithms under weak memory orderings
Ingår i SIGARCH Computer Architecture News, s. 65-71, 2008
Insights to Angluin's Learning
Ingår i Electr. Notes on Theoret. Comput. Sci., s. 3-18, 2005
Simulating perfect channels with probabilistic lossy channels
Ingår i Information and Computation, s. 22-40, 2005
Using Forward Reachability Analysis for Verification of Lossy Channel Systems
Ingår i Formal methods in system design, s. 39-65, 2004
Model checking of systems with many identical timed processes
Ingår i Theoretical Computer Science, s. 241-264, 2003
ASTEC: An Experience in the Establishment of Collaboration between Academia and Industry
Ingår i Springer International Journal on Software Tools for Technology Transfer, s. 401-404, 2003
Testing preorders for probabilistic processes can be characterized by simulations
Ingår i Theoretical Computer Science, s. 33-51, 2002
Algorithmic analysis of programs with well quasi-ordered domains
Ingår i INFORMATION AND COMPUTATION, s. 109-127, 2000
Proving Refinement Using Transduction
Ingår i Distributed Computing, s. 129-150, 1999
Verifying programs with unreliable channels
Ingår i Information and Computation, s. 91-101, 1996
Deciding Bisimulation Equivalences for a Class of Non-Finite-State Programs
Ingår i Information and Computation, s. 272-302, 1993
Kapitel i böcker, delar av antologi
Ingår i The Combined Power of Research, Education, and Dissemination, s. 259-279, Springer, 2025
Trading Space for Simplicity in Stateless Model Checking
Ingår i Real Time and Such, s. 79-97, Springer, 2024
Consistency and Persistency in Program Verification: Challenges and Opportunities
Ingår i Principles of Systems Design, s. 494-510, Springer, 2022
Comparing source sets and persistent sets for partial order reduction
Ingår i Models, Algorithms, Logics and Tools, s. 516-536, Springer, 2017
Learning of automata models extended with data
Ingår i Formal Methods for Eternal Networked Software Systems, s. 327-349, Springer Berlin/Heidelberg, 2011
Probabilistic Extensions of Process Algebras
s. 685-710, ELSEVIER, 2001
On the existence of network invariants for verifying parameterized systems
Ingår i Correct System Design, s. 180-197, Springer-Verlag, Berlin, 1999
Konferensbidrag
Testing IoT Protocol Requirements Using Fuzzing and Symbolic Execution: Application to CoAP
Ingår i 2024 IEEE Conference on Standards for Communications and Networking (CSCN), s. 48-54, 2024
Parsimonious Optimal Dynamic Partial Order Reduction
2024
Parsimonious Optimal Dynamic Partial Order Reduction
Ingår i COMPUTER AIDED VERIFICATION, PT II, CAV 2024, s. 19-43, 2024
- DOI för Parsimonious Optimal Dynamic Partial Order Reduction
- Ladda ner fulltext (pdf) av Parsimonious Optimal Dynamic Partial Order Reduction
Monitor-based Testing of Network Protocol Implementations Using Symbolic Execution
Ingår i 19TH INTERNATIONAL CONFERENCE ON AVAILABILITY, RELIABILITY, AND SECURITY, ARES 2024, 2024
SMBugFinder: An Automated Framework for Testing Protocol Implementations for State Machine Bugs
Ingår i PROCEEDINGS OF THE 33RD ACM SIGSOFT INTERNATIONAL SYMPOSIUM ON SOFTWARE TESTING AND ANALYSIS, ISSTA 2024, s. 1866-1870, 2024
Scalable Tree-based Register Automata Learning
Ingår i Tools and Algorithms for the Construction and Analysis of Systems, s. 87-108, 2024
- DOI för Scalable Tree-based Register Automata Learning
- Ladda ner fulltext (pdf) av Scalable Tree-based Register Automata Learning
Tailoring Stateless Model Checking for Event-Driven Multi-threaded Programs
Ingår i Automated Technology for Verification and Analysis, s. 176-198, 2023
- DOI för Tailoring Stateless Model Checking for Event-Driven Multi-threaded Programs
- Ladda ner fulltext (pdf) av Tailoring Stateless Model Checking for Event-Driven Multi-threaded Programs
Tailoring Stateless Model Checking for Event-Driven Multi-Threaded Programs
2023
An Active Learning Approach to Synthesizing Program Contracts
Ingår i Software Engineering and Formal Methods, SEFM 2023, s. 126-144, 2023
An Active Learning Approach to Synthesizing Program Contracts
2023
Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens
Ingår i 2022 Formal Methods in Computer-Aided Design (FMCAD), s. 284-293, 2022
- DOI för Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens
- Ladda ner fulltext (pdf) av Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens
Applying Symbolic Execution to Test Implementations of a Network Protocol Against its Specification
Ingår i 2022 IEEE 15TH INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION (ICST 2022), s. 70-81, 2022
DTLS-Fuzzer: A DTLS Protocol State Fuzzer
Ingår i 2022 IEEE 15th International Conference on Software Testing, Verification and Validation (ICST 2022), s. 456-458, 2022
Analysis of DTLS Implementations Using Protocol State Fuzzing
Ingår i Proceedings of the 29th USENIX Security Symposium, s. 2523-2540, 2020
Dynamic Partial Order Reduction Under the Release-Acquire Semantics (Tutorial)
Ingår i Networked Systems, s. 3-18, 2019
Optimal Stateless Model Checking under the Release-Acquire Semantics
Ingår i SPLASH OOPSLA 2018, Boston, Nov 4-9, 2018, 2018
Fragment abstraction for concurrent shape analysis
Ingår i Programming Languages and Systems, s. 442-471, 2018
Lock-free Contention Adapting Search Trees
Ingår i The 30th ACM Symposium on Parallelism in Algorithms and Architectures, SPAA 2018, 2018
Fine-grained local dynamic load balancing in PDES
Ingår i Proc. 6th ACM SIGSIM Conference on Principles of Advanced Discrete Simulation, s. 201-212, 2018
The Quest for Optimality in Stateless Model Checking of Concurrent Programs
Ingår i Formal Methods For Industrial Critical Systems, FMICS 2018, 2018
Extending Automata Learning to Extended Finite State Machines
Ingår i Machine Learning for Dynamic Software Analysis, s. 149-177, 2018
Optimal dynamic partial order reduction with observers
Ingår i Tools and Algorithms for the Construction and Analysis of Systems, s. 229-248, 2018
- DOI för Optimal dynamic partial order reduction with observers
- Ladda ner fulltext (pdf) av Optimal dynamic partial order reduction with observers
Ingår i Proc. 5th ACM SIGSIM Conference on Principles of Advanced Discrete Simulation, s. 53-64, 2017
Automated Verification of Linearization Policies
Ingår i Automated Verification of Linearization Policies, 2016
Stateless model checking for POWER
Ingår i Computer Aided Verification, s. 134-156, 2016
Industrial Evaluation of Test Suite Generation Strategies for Model-Based Testing
2016
Efficient inter-process synchronization for parallel discrete event simulation on multicores
Ingår i Proc. 3rd ACM SIGSIM Conference on Principles of Advanced Discrete Simulation, s. 183-194, 2015
Stateless model checking for TSO and PSO
Ingår i Tools and Algorithms for the Construction and Analysis of Systems, s. 353-367, 2015
Mediator synthesis in a component algebra with data
Ingår i Correct System Design, s. 238-259, 2015
RALib: A LearnLib extension for inferring EFSMs
2015
A Modeling Framework for Reuse Distance-based Estimation of Cache Performance
Ingår i Performance Analysis of Systems and Software (ISPASS), 2015 IEEE International Symposium on, s. 62-71, 2015
Learning Extended Finite State Machines
Ingår i Software Engineering and Formal Methods. 12th International Conference, SEFM 2014, s. 250-264, 2014
Optimal dynamic partial order reduction
Ingår i Proc. 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, s. 373-384, 2014
Ingår i Proc. 3rd International Conference on Sensor Networks, s. 28-40, 2014
Modeling cache coherence misses on multicores
Ingår i 2014 IEEE INTERNATIONAL SYMPOSIUM ON PERFORMANCE ANALYSIS OF SYSTEMS AND SOFTWARE (ISPASS), s. 96-105, 2014
An Integrated Specification and Verification Technique for Highly Concurrent Data Structures
Ingår i Tools and Algorithms for the Construction and Analysis of Systems, 2013
Verification of heap manipulating programs with ordered data by extended forest automata
Ingår i Automated Technology for Verification and Analysis, s. 224-239, 2013
- DOI för Verification of heap manipulating programs with ordered data by extended forest automata
- Ladda ner fulltext (pdf) av Verification of heap manipulating programs with ordered data by extended forest automata
A Skiplist-based Concurrent Priority Queue with Minimal Memory Contention
Ingår i OPODIS 2013: 17th International Conference On Principles Of DIstributed Systems, s. 206-220, 2013
Automated Mediator Synthesis: Combining Behavioural and Ontological Reasoning
Ingår i SEFM 2013, 11th Int. Conf. on Software Engineering and Formal Methods, s. 274-288, 2013
Assume-guarantee reasoning for safe component behaviours
Ingår i Formal Aspects of Component Software, s. 92-109, 2013
Inferring Canonical Register Automata
Ingår i Verification, Model Checking, and Abstract Interpretation - 13th International Conference,, s. 251-266, 2012
Demonstrating Learning of Register Automata
Ingår i Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference,, s. 466-471, 2012
A succinct canonical register automaton model for data domains with binary relations
Ingår i Automated Technology for Verification and Analysis, s. 57-71, 2012
Inferring semantic interfaces of data structures
Ingår i Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change, s. 554-571, 2012
A Compositional Specification Theory for Component Behaviours
Ingår i Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012,, s. 148-168, 2012
Ingår i Proc. 5th Swedish Workshop on Multi-Core Computing, 2012
Assume-Guarantee Reasoning for Safe Component Behaviours
Ingår i Proc. FACS: Formal Aspects of Component Software, 9th Int. Symp., s. 92-109, 2012
A succinct canonical register automaton model
Ingår i Automated Technology for Verification and Analysis, s. 366-380, 2011
On Handling Data in Automata Learning: Considerations from the CONNECT Perspective
Ingår i Leveraging Applications of Formal Methods, Verification, and Validation, s. 221-235, 2010
Generating Models of Infinite-State Communication Protocols Using Regular Inference with Abstraction
Ingår i Testing Software and Systems, s. 188-204, 2010
Inferring Compact Models of Communication Protocol Entities
Ingår i Leveraging Applications of Formal Methods, Verification, and Validation, s. 658-672, 2010
Using SPIN to model check concurrent algorithms, using a translation from C to Promela
Ingår i Proc. 2nd Swedish Workshop on Multi-Core Computing, s. 67-69, 2009
CONNECT Challenges: Towards Emergent Connectors for Eternal Networked Systems
Ingår i Proc. 14th International Conference on Engineering of Complex Computer Systems, s. 154-161, 2009
State-Space Exploration for Concurrent Algorithms under Weak Memory Orderings
Ingår i Proc. 1st Swedish Workshop on Multi-Core Computing, s. 82-88, 2008
Regular Inference for State Machines Using Domains with Equality Tests
Ingår i Fundamental Approaches to Software Engineering, s. 317-331, 2008
Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols
Ingår i Tools and Algorithms for the Construction and Analysis of Systems, s. 18-32, 2008
Cyclic dependencies in modular performance analysis
Ingår i Proc. 8th ACM International Conference on Embedded Software, s. 179-188, 2008
Systematic Acceleration in Regular Model Checking
Ingår i Computer Aided Verification, s. 131-144, 2007
Regular Inference for State Machines with Parameters.
Ingår i Fundamental Approaches to Software Engineering, 9th International Conference, FASE 2006,, s. 107-121, 2006
Proving Liveness by Backwards Reachability
2006
Inference of Event-Recording Automata using Timed Decision Trees
Ingår i International Conference on Concurrency Theory, 2006
Inference of Timed Transition Systems
Ingår i Proceedings of the 6th International Workshop on Verification of Infinite-State Systems (INFINITY), 2005
On the Correspondence Between Conformance Testing and Regular Inference
Ingår i FASE 2005, s. 175-189, 2005
Learning of event-recording automata
Ingår i FORMATS/FTRTFT 2004, s. 379-396, 2004
Specifying and Generating Test Cases Using Observer Automata
Ingår i Proceedings of the 4th International Workshop on Formal Approaches to Testing of Software, s. 125-139, 2004
Regular Model Checking for LTL(MSO)
Ingår i Computer Aided Verification, s. 348-360, 2004
A Survey of Regular Model Checking.
Ingår i CONCUR 2004 - Concurrency Theory, s. 35-48, 2004
Report on Dataflow Dependencies in Billing Processing Systems
Ingår i Proc. ISoLA '04: 1st International Symposium on Leveraging Applications of Formal Methods, 2004
Extracting the Process Structure of Erlang Applications
Ingår i Erlang Workshop, Firenze, Sept. 2, 2002
Extracting the process structure of Erlang applications
Ingår i Proc. Erlang Workshop, Firenze, Italy, 2001
Ingår i Proc. 12th Int. Conf. on Computer Aided Verification, 2000
Fully Abstract Characterization of Probabilistic May Testin
1999
A general approach to partial order reductions in symbolic verification
Ingår i Computer Aided Verification, s. 379-390, 1998
Verifying networks of timed processes
Ingår i Tools and Algorithms for the Construction and Analysis of Systems, s. 298-312, 1998
Undecidable verification problems for programs with unreliable channels
Ingår i Automata, Languages and Programming, s. 71-90, 1996
Automata-Based Automated Detection of State Machine Bugs in Protocol Implementations
Ingår i Proc. 30th Annual Network and Distributed System Security Symposium, NDSS
Proceedings (redaktörskap)
Rapporter
A Skiplist-Based Concurrent Priority Queue with Minimal Memory Contention
2018
A Skiplist-Based Concurrent Priority Queue with Minimal Memory Contention
2018
Active Learning for Extended Finite State Machines
2015
Learning Extended Finite State Machines (extended version)
2015
Forecasting Lock Contention Before Adopting Another Lock Algorithm
2015
An Algebraic Theory of Interface Automata
2013
A Compositional Specification Theory for Component Behaviours
2012
Learning of Event-Recording Automata
2008
Inference of Event-Recording Automata using Timed Decision Trees
2008
Regular Inference for Communication Protocol Entities
2008
Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols: (Extended Version)
2007
Insights to Angluin's Learning
2003