Publications by Bengt Jonsson

My publication list in the DBLP publication server

2023

• Paul Fiterau-Brostean, Bengt Jonsson, Konstantinos Sagonas, and Fredrik Tå{\aa}quist. Automata-based automated detection of state machine bugs in protocol implementations. in NDSS 2023. 30th Annual Network and Distributed System Security Symposium, , San Diego, California, USA, February 27 - March 3, The Internet Society, 2023.
  DOI | PDF | Artifact
• Parosh Aziz Abdulla, Mohamed Faouzi Atig, Frederik Meyer Bønneland, Sarbojit Das, Bengt Jonsson, Magnus Lång, and Konstantinos Sagonas. Tailoring Stateless Model Checking for Event-Driven Multi-Threaded Programs. in ATVA 2023. 21st International Symposium on Automated Technology for Verification and Analysis, pages 176-198, October 2023.
  DOI | Preprint with Proofs
• Sandip Ghosal, Bengt Jonsson, and Philipp Ruemmer. An Active Learning Approach to Synthesizing Program Contracts. in SEFM 23. 21st International Conference on Software Engineering and Formal Methods. LNCS 14323, pp. 126-144. November 2023.
  DOI | [author version]

• H. Asadian, P. Fiterau-Brostean, B. Jonsson, and K. Sagonas. Applying Symbolic Execution to Test Implementations of a Network Protocol Against its Specification. in ICST 2022. 15th IEEE Int. Conf. on Software Testing, Verification and Validation. Valencia, Spain, April 4-14, 2022, pages 70--81. IEEE, 2022.
  DOI | [PDF] | Replication Material
• Paul Fiterau-Brostean, Bengt Jonsson, Konstantinos Sagonas, and Fredrik Tåquist. DTLS-fuzzer: A DTLS protocol state fuzzer. in ICST 2022. 15th IEEE Int. Conf. on Software Testing, Verification and Validation. Valencia, Spain, April 4-14, 2022, pages 456--458. IEEE, 2022.
  DOI | [PDF] | [Demo Video]
• Bengt Jonsson, Magnus Lång, and Konstantinos Sagonas. Awaiting for Godot: Stateless model checking that avoids executions where nothing happens. in FMCAD 2022. 22nd Formal Methods in Computer-Aided Design, Trento, Italy, October 17-21, 2022, pages 284--293. {IEEE}, 2022.
  DOI | Preprint with Proofs

• K. Winblad, K. Sagonas, and B. Jonsson. Lock-free Contention Adapting Search Trees. ACM Trans. Parallel Comput.8(2): 10:1-10:38 (2021)
  DOI | [author version]

• P. Fiterau-Brostean, B. Jonsson, R. Merget, J. de Ruiter, K. Sagonas, and J. Somorovsky. Analysis of DTLS Implementations Using Protocol State Fuzzing. 29th USENIX Security Symposium 2020
  Open Access

• P. Abdulla, M. Faouzi Atig, B. Jonsson, M. Lång, T. Phong Ngo, and K. Sagonas. Optimal stateless model checking for reads-from equivalence under sequential consistency. PACMPL 3(OOPSLA): 150:1-150:29 (2019)
  DOI | [author version]
• P. Abdulla, M. Faouzi Atig, B. Jonsson, and T. Phong Ngo. Dynamic Partial Order Reduction Under the Release-Acquire Semantics (Tutorial). In Networked Systems, 7th International Conference, NETYS 2019, Marrakech, Morocco, June 19-21, 2019. LNCS 11704, Springer 2019.
  DOI
• J. Lindén, P. Bauer, S. Engblom, B. Jonsson. Exposing Inter-process Information for Efficient PDES of Spatial Stochastic Systems on Multicores. ACM Trans. Model. Comput. Simul. 29(2): 11:1-11:25 (2019)
  DOI | [author version],
• F. Howar, B. Jonsson, F. Vaandrager. Combining Black-Box and White-Box Techniques for Learning Register Automata In Computing and Software Science - State of the Art and Perspectives, LNCS 10000, pp 563-588, Springer 2019.
  DOI | [author version]

• P. Abdulla, M. Faouzi Atig, B. Jonsson, and T. Phong Ngo. Optimal stateless model checking under the release-acquire semantics. PACMPL, 2 (OOPSLA):135:1--135:29, 2018.
  DOI | [author version]
• S. Cassel, F. Howar, B. Jonsson, B. Steffen. Extending Automata Learning to Extended Finite State Machines In Machine Learning for Dynamic Software Analysis: Potentials and Limits, LNCS 11026, pp 149-177, Springer 2018.
  DOI | [author version]
• S. Aronis, B. Jonsson, M. Lång, K. Sagonas. Optimal Dynamic Partial Order Reduction with Observers In TACAS 2018: Proc. Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems, LNCS 10806, pp 229-248, Springer 2018.
  DOI | [author version],
• P.A. Abdulla, B. Jonsson, C.Q. Trinh, Fragment Abstraction for Concurrent Shape Analysis In ESOP 2018: Proc. 27th European Symp. on Programming, LNCS 10801, pp 442-471, Springer 2018.
  DOI | [author version],
• J. Lindén, P. Bauer, S. Engblom, B. Jonsson. Fine-Grained Local Dynamic Load Balancing in PDES. In SIGSIM PADS 2018, ACM SIGSIM Conf. on Principles of advanced Discrete Simulation, May 23-25, 2018, Rome, pp 201-212.
  DOI | [author version],
• K. Winblad, K. Sagonas, B. Jonsson. Lock-free Contention Adapting Search Trees In SPAA '18: 30th ACM Symposium on Parallelism in Algorithms and Architectures, Vienna, Austria, July 16 - 18, 2018, pp 121-132.
  DOI | [author version],

• P.A. Abdulla, S. Aronis, M. Faouzi Atig, B. Jonsson, C. Leonardsson, K. Sagonas. Stateless Model Checking for TSO and PSO. Acta Informatica 54(8) pp 789-818, Dec. 2017.
  DOI | earlier version as [technical report]
• P.A. Abdulla, S. Aronis, B. Jonsson, K. Sagonas. Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction. Journal of the ACM 64(4):25:1--25:49, 2017.
  DOI | author version,
• P.A. Abdulla, F. Haziza, L. Holík, B. Jonsson, and A. Rezine. An Integrated Specification and Verification Technique for Highly Concurrent Data Structures. Journal of Software Tools for Technology Transfer, 19(5):549--563, 2017.
  DOI | [author version]
• P.A. Abdulla, S. Aronis, B. Jonsson, K. Sagonas. Source Sets: Comparing Source Sets and Persistent Sets for Partial Order Reduction. In Models, Algorithms, Logics and Tools - Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday, LNCS 10460, pp 516-536, Springer 2017.
  DOI | [similar author version],
• J. Lindén, P. Bauer, S. Engblom, B. Jonsson. Exposing Inter-Process Information for Efficient Parallel Discrete Event Simulation of Spatial Stochastic Systems. In SIGSIM PADS 2017, ACM SIGSIM Conf. on Principles of advanced Discrete Simulation, May 24-26, 2017, Singapore.
  DOI | [author version],

• P.A. Abdulla, B. Jonsson, C.Q. Trinh, Automated Verification of Linearization Policies. In SAS 2016: Proc. 23rd Static Analysis Symposium, 2016, LNCS 9837, pp 61-83, Springer 2016.
  DOI |[author version],
• P.A. Abdulla, M. Faouzi Atig, B. Jonsson, C. Leonardsson. Stateless Model Checking for POWER. In CAV 2016: Proc. 19th Int. Conf. on Computer Aided Verification, 2016 LNCS 9780, pp 134-156, Springer 2016.
  DOI extended version as [technical report]
• S. Cassel, F. Howar, B. Jonsson, B. Steffen. Active Learning for Extended Finite State Machines Formal Aspects of Computing, 28(2): 233-263 (2016).
  DOI, preliminary version as Technical Report 2015-032
• P.A. Abdulla, L. Holík, B. Jonsson, O. Lengál, C.Q. Trinh, T. Vojnar, Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. Acta Informatica, 53(4):357-384, June 2016.
  DOI | earlier version as Technical Report version (technical report FIT-TR-2013-02, Brno, CZ, FIT VUT, 2013)
• J. Blom, B. Jonsson, S.-O. Nyström, Industrial Evaluation of Test Suite Generation Strategies for Model-Based Testing in A-MOST 2016: 12th Advances in Model based Testing Workshop, Chicago, April 11, 2016.
  Electronic Edition | [author version],

• F. Aarts, B. Jonsson, J. Uijen, F.W. Vaandrager. Generating Models of Infinite-State Communication Protocols Using Regular Inference with Abstraction Formal Methods in System Design, 46(1):1-41, 2015.
  DOI, earlier version as Technical report ICIS-R13001, Radboud University Nijmegen, January 2013
• P. Bauer, J. Lindén, S. Engblom, B. Jonsson. Efficient Inter-Process Synchronization for Parallel Discrete Event Simulation on Multicores. In SIGSIM PADS 2015, ACM SIGSIM Conf. on Principles of advanced Discrete Simulation, June 15-17, 2015, London, UK.
  DOI, [author version],
• P.A. Abdulla, S. Aronis, M. Faouzi Atig, B. Jonsson, C. Leonardsson, K. Sagonas. Stateless Model Checking for TSO and PSO. In TACAS 2015: Proc. Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems, 2015, LNCS 9035, pp 353-367, Springer 2015.
  DOI, extended version as [technical report]
• P. Xiaoyue, B. Jonsson A Modeling Framework for Reuse Distance-based Estimation of Cache Performance In ISPASS 2015, IEEE International Symposium on Performance Analysis of Systems and Software, March 29-31, 2015, Philadelphia, PA
  DOI, [author version],
• S. Cassel, F. Howar, B. Jonsson, M. Merten, B. Steffen. A Succinct Canonical Register Automaton Model Journal of Logic and Algebraic Programming 84(1): 54-66, Elsevier, Jan. 2015.
  DOI, manuscript as Technical Report 2013-026
• S. Cassel, F. Howar, B. Jonsson. RALib: A LearnLib extension for inferring EFSMs In DIFTS 15, Int. Workshop on Design and Implementation of Formal Tools and Systems, Austin, Texas USA, September 26-27, 2015.
  [online proceedings]
• L. Holík, M. Isberner, B. Jonsson. Mediator Synthesis in a Component Algebra with Data in Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Oldenburg LNCS 9369, pp 238-259, Springer 2015.
  DOI | [author version],

• P. Axer, R. Ernst, H. Falk, A. Girault, D. Grund, N. Guan, B. Jonsson, P. Marwedel, J. Reineke, C. Rochange, M. Sebastian, R. v. Hanxleden, R. Wilhelm, W. Yi. Building Timing Predictable Embedded Systems. ACM Trans. on Embedded Computing Systems 13(4):82, 2014.
  ACM DL page, manuscript as Technical Report 2012-013
• C. Chilton, B. Jonsson, M.Z. Kwiatkowska. An Algebraic Theory of Interface Automata. Theoretical Computer Science 549: 146-174, Elsevier 2014.
  DOI, [author version], earlier version as Technical Report CS-RR-13-02, Dept. of Computer Science, University of Oxford.
• S. Cassel, F. Howar, B. Jonsson, B. Steffen. Learning Extended Finite State Machines In SEFM 2014, 12th Int. Conf. on Software Engineering and Formal Methods, LNCS 8702, pp 250-264, Springer 2014.
  DOI, [author version], extended revised version as Technical Report 2015-032
• C. Chilton, B. Jonsson, M.Z. Kwiatkowska. Compositional Assume-Guarantee Reasoning for Input/Output Component Theories Science of Computer Programming 91(Part A): 115-137, Elsevier, Oct. 2014.
  DOI 10.1016/j.scico.2013.12.010, [author version],
• P.A. Abdulla, S. Aronis, B. Jonsson, K. Sagonas. Optimal Dynamic Partial Order Reduction. In POPL '14: 41st ACM Symp. on Principles of Programming Languages, pp. 373-384, 2014.
  DOI 10.1145/2535838.2535845, similar version (with appendix),
• F. H. Bijarbooneh, A. Pathak, J. Pearson, V. Issarny, B. Jonsson. A Constraint Programming Approach for Managing End-to-end Requirements in Sensor Network Macroprogramming In SensorNets 2014: 3rd Int. Conf. on Sensor Networks, Lisbon Portugal, 2014.
  DOI, [author version],
• P. Xiaoyue, B. Jonsson Modelling Coherence Cache Misses on Multi-core with Reuse Distance. In ISPASS 2014, IEEE International Symposium on Performance Analysis of Systems and Software, March 23-25, 2014 Monterey, CA, pp. 96-105.
  DOI, [author version],

• J. Lindén, B. Jonsson. A Skiplist-based Concurrent Priority Queue with Minimal Memory Contention. in OPODIS 2013: 17th International Conference On Principles Of DIstributed Systems December 16-18, Nice, France. LNCS 8304, pp. 206-220, Springer, 2013.
  DOI 10.1007/978-3-319-03850-6_15, Extended version as Technical Report 2013-025, also with Code and SPIN model for the algorithm.
• P.A. Abdulla, L. Holík, B. Jonsson, O. Lengál, C.Q. Trinh, T. Vojnar, Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. In ATVA 2013, Proc. Int. Symp. Automated Technology for Verification and Analysis LNCS 8172, pp. 224-239, Springer, 2013.
  DOI 10.1007/978-3-319-02444-8_17, [author version], Extended version (technical report FIT-TR-2013-02, Brno, CZ, FIT VUT, 2013)
• A. Bennaceur, C. Chilton, M. Isberner, B. Jonsson. Automated Mediator Synthesis: Combining Behavioural and Ontological Reasoning. In SEFM 2013, 11th Int. Conf. on Software Engineering and Formal Methods, LNCS 8137, pp 274-288, Springer 2013.
  DOI 10.1007/978-3-642-40561-7_19, [author version],
• P.A. Abdulla, F. Haziza, L. Holík, B. Jonsson, and A. Rezine. An Integrated Specification and Verification Technique for Highly Concurrent Data Structures. In TACAS 2013: Proc. Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems, LNCS 7795: 324-338. Springer, 2013.
  DOI 10.1007/978-3-642-36742-7_23, [author version]
• C. Chilton, B. Jonsson, M.Z. Kwiatkowska. An Algebraic Theory of Interface Automata. Technical Report CS-RR-13-02, Department of Computer Science, University of Oxford.

• B. Jonsson. Using refinement calculus techniques to prove linearizability. Formal Asp. Comput., 24(4-6):537-554 (2012)
  DOI 10.1007/s00165-012-0250-7, [author version],
• P.A. Abdulla, B. Jonsson, Marcus Nilsson, Julien d'Orso, and M. Saksena. Regular model checking for LTL(MSO). Journal of Software Tools for Technology Transfer, 14(2): 223-241 (2012)
  DOI 10.1007/s10009-011-0212-z, [author version],
• F. Howar, M. Isberner, B. Steffen, O. Bauer, B. Jonsson. Inferring Semantic Interfaces of Data Structures. InProc. ISoLA (1): Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change - 5th Int. Symp.. LNCS 7609: 554-571. Springer, 2012.
  DOI 10.1007/978-3-642-34026-0_41, [author version],
• S. Cassel, B. Jonsson, F. Howar, B. Steffen. A Succinct Canonical Register Automaton Model for Data Domains with Binary Relations. In ATVA 2012, Proc. Int. Symp. Automated Technology for Verification and Analysis, LNCS 7561: 57-71. Springer, 2012.
  DOI 10.1007/978-3-642-33386-6_6, [author version],
• C. Chilton, B. Jonsson, M.Z. Kwiatkowska. Assume-Guarantee Reasoning for Safe Component Behaviours. In Proc. FACS: Formal Aspects of Component Software, 9th Int. Symp., LNCS 7684: 92-109. Springer, 2012.
  DOI 10.1007/978-3-642-35861-6_6, [author version],
• T. Chen, C. Chilton, B. Jonsson, M.Z. Kwiatkowska. A Compositional Specification Theory for Component Behaviours. In Proc. ESOP: European Symposium on Programming, LNCS 7211: 148-168. Springer, 2012.
  DOI 10.1007/978-3-642-28869-2_8, [author version], extended version as Technical report CS-RR-12-01, University of Oxford.
• M. Merten, F. Howar, B. Steffen, S. Cassel, B. Jonsson. Demonstrating Learning of Register Automata. In TACAS 2012: Proc. Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems, LNCS 7214: 466-471. Springer, 2012.
  DOI 10.1007/978-3-642-28756-5_32, [author version],
• F. Howar, B. Steffen, B. Jonsson, S. Cassel. Inferring Canonical Register Automata In VMCAI 2012 Proc. 13th Int. Conf. on Verification, Model Checking, and Abstract Interpretation. LNCS 7148:251-266, Springer Verlag, 2012.
  DOI 10.1007/978-3-642-27940-9_17, [author version],

• Bengt Jonsson Learning of Automata Models Extended with Data in Marco Bernardo, Valérie Issarny (Eds.): Formal Methods for Eternal Networked Software Systems - 11th International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM 2011. Bertinoro, Italy, June 13-18, 2011. LNCS 6659 pp. 327-349, Springer 2011
  DOI 10.1007/978-3-642-21455-4_10, [author version],
• Sofia Cassel, Falk Howar, Bengt Jonsson, Maik Merten, Bernhard Steffen. A Succinct Canonical Register Automaton Model In ATVA 2011, Proc. Int. Symp. Automated Technology for Verification and Analysis, LNCS 6996: 366-380. Springer, 2011.
  DOI 10.1007/978-3-642-24372-1_26, [author version], extended version as Technical Report 2013-026

• Olga Grinchtein, Bengt Jonsson, Martin Leucker. Learning of event-recording automata Theor. Comput. Sci. 411(47): 4029-4054 (2010)
  DOI 10.1016/j.tcs.2010.07.008, [author version],
• F. Aarts, B. Jonsson, J. Uijen Generating Models of Infinite-State Communication Protocols Using Regular Inference with Abstraction In ICTSS 2010, 22nd IFIP WG 6.1 Int. Conf. Testing Software and Systems, Natal, Brazil, LNCS 6435: 188-204, Springer 2010
  DOI 10.1007/978-3-642-16573-3_14, [author version], extended version as Technical report ICIS-R13001, Radboud University Nijmegen, January 2013
• T. Bohlin, B. Jonsson, S. Soleimanifard Inferring Compact Models of Communication Protocol Entities In ISoLA 2010, 4th Int. Symp. on Leveraging Applications of Formal Methods, Verification, and Validation, Part I, Heraklion, Crete, October 18-21, 2010, LNCS 6415: 658-672, Springer 2010
  DOI 10.1007/978-3-642-16558-0_53, [author version],
• Falk Howar, Bengt Jonsson, Maik Merten, Bernhard Steffen, Sofia Cassel. On Handling Data in Automata Learning - Considerations from the CONNECT Perspective In ISoLA 2010, 4th Int. Symp. on Leveraging Applications of Formal Methods, Verification, and Validation, Part II, Heraklion, Crete, October 18-21, 2010. LNCS 6416: 221-235, Springer 2010
  DOI 10.1007/978-3-642-16561-0_24, [author version],

• V. Issarny, B. Steffen, B. Jonsson, G.S. Blair, P. Grace, M.Z. Kwiatkowska, R. Calinescu, P. Inverardi, M. Tivoli, A. Bertolino, A. Sabetta. CONNECT Challenges: Towards Emergent Connectors for Eternal Networked Systems. In ICECCS 2009: 14th IEEE International Conference on Engineering of Complex Computer Systems, Potsdam, Germany, 2-4 June 2009. pp. 154-161, IEEE Computer Society 2009.
  DOI 10.1109/ICECCS.2009.44

• T. Berg, B. Jonsson, H. Raffelt Regular Inference for State Machines Using Domains with Equality Tests. In Proc. FASE '08, 11th Int. Conf. on Fundamental Approaches to Software Engineering, LNCS 3961:317-331 (2008).
  DOI 10.1007/978-3-540-78743-3_24, [(extended) author version],
• M. Saksena, O. Wibling, and B. Jonsson Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols. In Proc. TACAS 2008, 14th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 4963: 18-32, Springer-Verlag, 2008.
  DOI 10.1007/978-3-540-78800-3_3, [author version], [extended version (with proofs)],
• B. Jonsson, S. Perathoner, L. Thiele, and W. Yi. Cyclic dependencies in modular performance analysis. In EMSOFT '08: Embedded Software, 8th Int. Conf., pp. 179-188. ACM Press, 2008.
  DOI 10.1145/1450058.1450083, [author version],
• B. Jonsson. State-space exploration for concurrent algorithms under weak memory orderings SIGARCH Computer Architecture News 36(5): 65-71 (2008)
  DOI 10.1145/1556444.1556453, [author version],

• B. Jonsson, and M. Saksena. Systematic Acceleration in Regular Model Checking. In CAV 2007: Proc. 19th Int. Conf. on Computer Aided Verification, LNCS 4590: 131-144 (2007).
  DOI 10.1007/978-3-540-73368-3_16, [author version],

• O. Grinchtein, B. Jonsson, P. Pettersson. Inference of Event-Recording Automata Using Timed Decision Trees. In Proc. CONCUR 2006, 15th Int. Conf. on Concurrency Theory, LNCS 4137: 435-449 (2006)
  DOI 10.1007/11817949_29, [author version],
• P.A. Abdulla, B. Jonsson, A. Rezine, M. Saksena. Proving Liveness by Backwards Reachability. In Proc. CONCUR 2006, 15th Int. Conf. on Concurrency Theory, LNCS 4137: 95-109 (2006).
  DOI 10.1007/11817949_7, [author version],
• T. Berg, B. Jonsson, H. Raffelt. Regular Inference for State Machines with Parameters. In Proc. FASE '06, 9th Int. Conf. on Fundamental Approaches to Software Engineering, LNCS 3922: 107-121 (2006).
  DOI 10.1007/11693017_10, [author version],

• M. Broy, B. Jonsson, J.-P. Katoen, M. Leucker, A. Pretschner (Eds.) Model-Based Testing of Reactive Systems, Advanced Lectures LNCS 3472, Springer 2005
• P.A. Abdulla, C. Baier, P. Iyer, and B. Jonsson. Simulating perfect channels with probabilistic lossy channels. Information and Computation, 197(1-2):22--40, 2005.
  DOI 10.1016/j.ic.2004.12.001, [author version],
• T. Berg, O. Grinchtein, B. Jonsson M. Leucker, M. Leucker, and B. Steffen. On the correspondence between conformance testing and regular inference In Proc. FASE '05, 8th Int. Conf. on Fundamental Approaches to Software Engineering, LNCS 344: 175-189 (2005).
  DOI 10.1007/978-3-540-31984-9_14, [author version],
• O. Grinchtein, B. Jonsson, M. Leucker Inference of Timed Transition Systems. Electr. Notes Theor. Comput. Sci. 138(3): 87-99 (2005)
  DOI 10.1016/j.entcs.2005.02.062, [author version],
• T. Berg, B. Jonsson, M. Leucker, and M. Saksena. Insights to Angluin's learning. In Proc. Int. Workshop on Software Verification and Validation (SVV 2003), Electr. Notes Theor. Comput. Sci. 118: 3-18 (2005)
  DOI 10.1016/j.entcs.2004.12.015, [author version],

• Using forward reachability analysis for verification of lossy channel
  Parosh Aziz Abdulla, Aurore Annichini, and Ahmed Bouajjani.
  Formal Methods in System Design, 25(1):39--65, 2004.
• A survey of regular model checking.
  P.A. Abdulla, B. Jonsson, Marcus Nilsson, and M. Saksena.
  In Proc. CONCUR 2004, 15th Int. Conf. on Concurrency Theory, volume 3170 of LNCS, pages 348--360, 2004.
• Regular model checking for MSO + LTL.
  P.A. Abdulla, B. Jonsson, Marcus Nilsson, Julien d'Orso, and M. Saksena.
  In Proc. 16th Int. Conf. on Computer Aided Verification, pages 348--360, 2004.
• Learning of event-recording automata.
  O. Grinchtein, B. Jonsson, and M. Leucker.
  In FORMATS/FTRTFT, volume 3253 of Lecture Notes in Computer Science, pages 379--396. Springer Verlag, 2004.
• Specifying and generating test cases using observer automata.
  J. Blom, A. Hessel, B. Jonsson, and P. Pettersson.
  In Proc. FATES, 4th. International Workshop on Formal Approaches to Testing of Software, volume 3395 of Lecture Notes in Computer Science, pages 125--139. Springer Verlag, 2004.

• Generating on-line test oracles from temporal logic specifications.
  J. Håkansson, B. Jonsson, and O. Lundqvist.
  Journal of Software Tools for Technology Transfer,
  4(4):456--471, 2003.
  DOI, [author version]
• Model checking of systems with many identical timed processes.
  Parosh Aziz Abdulla and Bengt Jonsson.
  Theoretical Computer Science, 290(1):241--264, 2003.
• Automated test generation for industrial Erlang applications.
  J. Blom and B. Jonsson.
  In Proc. 2003 ACM SIGPLAN workshop on Erlang, pages 8--14, Uppsala, Sweden, Aug. 2003.
• Algorithmic improvements in regular model checking.
  Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, and Julien d'Orso.
  In Proc. 15th Int. Conf. on Computer Aided Verification, volume 2725 of LNCS, pages 236--248, 2003.

• Regular tree model checking.
  Parosh Aziz Abdulla, Bengt Jonsson, Pritha Mahata, and Julien d'Orso.
  In Proc. 14th Int. Conf. on Computer Aided Verification, volume 2404 of LNCS, 2002.
• Testing preorders for probabilistic processes can be characterized by
  B. Jonsson and W. Yi.
  Theoretical Computer Science, 282(1):33--51, 2002.
• Regular model checking made simple and efficient.
  Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, and Julien d'Orso.
  \newblock In Proc. CONCUR 2002, 13th Int. Conf. on Concurrency, volume 2421 of LNCS, pages 116--130, 2002.
• Processor pipelines and their properties for static WCET analysis.
  J. Engblom and B. Jonsson.
  In A. Sangiovanni-Vincentelli and J. Sifakis, editors, Embedded Software, 2th Int. Conf., volume 2491 of Lecture Notes in Computer Science, pages 334--348. Springer Verlag, 2002.
• Eliminating queues from RT UML model representations.
  Werner Damm and Bengt Jonsson.
  LNCS, 2469:375--394, 2002.

• Channel representations in protocol verification.
  Parosh Aziz Abdulla and Bengt Jonsson.
  In Proc. CONCUR 2001, 12th Int. Conf. on Concurrency, volume 2154 of LNCS, pages 1--15, 2001.
• An execution semantics for MSC-2000.
  B. Jonsson and G. Padilla.
  In R. Reed and J. Reed, editors, Proc. 10th SDL Forum: SDL 2001: Meeting UML, volume 2078 of Lecture Notes in Computer Science, pages 365--378, Copenhagen, Denmark, June 2001. Springer Verlag.
• Extracting the process structure of erlang applications.
  J. Nyström} and B. Jonsson.
  In Proc. Erlang Workshop, Firenze, Italy, Sept. 2001.
• Incremental requirement specification for evolving systems.
  B. Jonsson, T. Margaria, G. Naeser, J. Nyström, and B. Steffen.
  Nordic Journal of Computing, 8(1):65--87, 2001.
• Ensuring completeness of symbolic verification methods for infinite-state systems.
  Parosh Aziz Abdulla and Bengt Jonsson.
  Theoretical Computer Science, 256:145--167, 2001.

• Algorithmic analysis of programs with well quasi-ordered domains.
  Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Tsay Yih-Kuen.
  Information and Computation, 160:109--127, 2000.
  
• Regular model checking.
  A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili.
  In Emerson and Sistla, editors, Proc. 12th Int. Conf. on Computer Aided Verification, volume 1855 of Lecture Notes in Computer Science, pages 403--418. Springer Verlag, 2000.
• Using Forward Reachability Analysis for Verification of Lossy Channel Systems.
  Parosh Aziz Abdulla, A. Annichini, Ahmed Bouajjani, Bengt Jonsson.
  submitted for journal publication.
• Model checking of systems with many identical timed processes.
  P. Abdulla, and B. Jonsson.
  submitted for journal publication.
• Abstraction of communication channels in Promela: A case study.
  E. Fersman and B. Jonsson.
  In K. Havelund, J. Penix, and W. Visser, editors, SPIN Model Checking and Software Verification: Proc. 7th Int. SPIN Workshop, volume 1885 of LNCS, pages 187-204, Stanford, CA, 2000. Springer Verlag.
• Reasoning about probabilistic lossy channel systems.
  P. Abdulla, C. Baier, Purushothaman Iyer, B. Jonsson.
  In C. Palamidessi, editor, Proc. CONCUR 2000: 11th Int. Conf. on Concurrency Theory, volume 1877 of Lecture Notes in Computer Science, 2000.
• Regular model checking.
  A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili.
  In Emerson and Sistla, editors, Proc. 12th Int. Conf. on Computer Aided Verification, volume 1855 of Lecture Notes in Computer Science, pages 403-418, 2000.
• Incremental requirement specification for evolving systems.
  B. Jonsson, T. Margaria, G. Naeser, J. Nyström, and B. Steffen.
  In M. Calder and E. Magill, editors, Feature Interactions in Telecommunications and Software Systems VI, pages 145-162. IOS Press, 2000.
• Transitive closures of regular relations for verifying infinite-state systems.
  Bengt Jonsson and Marcus Nilsson.
  In S. Graf and M. Schwartzbach, editors Proc. TACAS '00, 6th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 1785 of LNCS,, 2000, Springer Verlag.

• Proving refinement using transduction.
  B. Jonsson, A. Pnueli, and C. Rump.
  Distributed Computing, 12(2-3):129-149, 1999.
• On modelling feature interactions in telecommunications.
  B. Jonsson, T. Margaria, G. Naeser, J. Nyström, and B. Steffen.
  In 11th Nordic Workshop on Programming Theory, Uppsala, Sweden., Oct. 1999.
• On the existence of network invariants for verifying parameterized systems.
  P. Abdulla, B. Jonsson.
  In Olderog and Steffen eds. Correct System Design - Recent Insights and Advances, volume 1710 of Lecture Notes in Computer Science, pages 180-197, 1999.
• Building tools for creation and analysis of telephone services.
  G. Naeser, J. Nyström, and B. Jonsson.
  In Proceedings of RVK '99, RadioVetenskap och Kommunikation'99, Karlskrona, Sweden, June 1999.
• A case study in automated detection of service interactions.
  G. Naeser, J. Nyström, and B. Jonsson.
  In Proceedings of RVK '99, RadioVetenskap och Kommunikation'99, Karlskrona, Sweden, June 1999.
• Handling global conditions in parameterized system verification.
  P. Abdulla, A. Bouajjani, B. Jonsson, and M. Nilsson.
  In Halbwachs and Peled, editors, Proc. 11th Int. Conf. on Computer Aided Verification, volume 1633 of Lecture Notes in Computer Science, pages 134-145, 1999.
• Fully abstract characterization of probabilistic may testing.
  B. Jonsson and W. Yi.
  In Katoen, editor, ARTS'99, Formal Methods for Real-Time and Probabilistic Systems, 5th Int. AMAST Workshop, volume 1601 of LNCS, pages 1-18. Springer Verlag, 1999.

• A fully abstract semantics for concurrent constraint programming.
  S.-O. Nyström and B. Jonsson.
  Information and Computation, 146:138-180, Nov. 1998.
• Partial Order Reductions for Timed Systems.
  J. Bengtsson, B. Jonsson, J. Lilius, W. Yi.
  In Proc. CONCUR'98: 9th Int. Conf. on Concurrency Theory, volume 1466 of LNCS, pages 485-500, 1998.
• On-the-fly analysis of systems with unbounded, lossy FIFO channels.
  Parosh Aziz Abdulla, Ahmed Bouajjani, and Bengt Jonsson.
  In Proc. 10th Int. Conf. on Computer Aided Verification, volume 1427 of LNCS, pages 305-318, 1998.
• A general approach to partial order reductions in symbolic verification.
  Parosh Aziz Abdulla, Bengt Jonsson, Mats Kindahl, and Doron Peled.
  In Proc. 10th Int. Conf. on Computer Aided Verification, volume 1427 of LNCS, pages 379-390, 1998.
• Verifying networks of timed processes.
  Parosh Aziz Abdulla and Bengt Jonsson.
  In Bernhard Steffen, editor, Proc. TACAS '98, 4th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 1384 of LNCS, pages 298-312, 1998.

• Modelling and automated verification of authentication protocols.
  Parosh Aziz Abdulla, Bengt Jonsson, and Aletta Nylen.
  In Proceedings of Dimacs workshop on design and formal verification of security protocols, 1997.

• Assumption/guarantee specifications in linear-time temporal logic.
  Bengt Jonsson and Yih-Kuen Tsay.
  Theoretical Computer Science, 167(1-2):47-72, 30 October 1996
• Undecidable verification problems for programs with unreliable channels.
  Parosh Aziz Abdulla and Bengt Jonsson.
  Information and Computation, 130(1):71-90, October 10, 1996.
  abstract
• Verifying programs with unreliable channels.
  Parosh Aziz Abdulla and Bengt Jonsson.
  Information and Computation, 127(2):91-101, June 15, 1996.
  abstract
• Creation of dependent features.
  J. Blom, R. Bol, B. Jonsson, and J. Nyström.
  In Proceedings of RVK '96, RadioVetenskap och Kommunikation'96, Luleå, Sweden, June 1996.
• Constraint oriented temporal logic specification.
  J. Blom and B. Jonsson.
  In M. Broy, S. Merz, and K. Spies, editors, Formal Systems Specification, The RPC-Memory Specification Case Study, volume 1169 of LNCS, pages 161-182. Springer Verlag, 1996.
• General decidability theorems for infinite-state systems.
  Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Tsay Yih-Kuen.
  In Proc. 11th IEEE Int. Symp. on Logic in Computer Science, pages 313-321, 1996. abstract
• A formalization of service independent building blocks.
  J. Nyström and B. Jonsson.
  In T. Margaria, editor, Proc. International Workshop on Advanced Intelligen Networks, pages 1-14, Passau, Germany, March 1996.

• Verifying safety properties of a class of infinite-state distributed algorithms.
  Bengt Jonsson and Lars Kempe.
  In Proc. 7th Int. Conf. on Computer Aided Verification, volume 939 of LNCS, pages 42-53. Springer Verlag, 1995.
  abstract | full version: postscript
• Compositional testing preorders for probabilistic processes.
  B. Jonsson and W. Yi.
  In Proc. 10th IEEE Int. Symp. on Logic in Computer Science, pages 431-441, 1995.
• Assumption/guarantee specifications in linear-time temporal logic.
  Bengt Jonsson and Yih-Kuen Tsay.
  In Mosses, Nielsen, and Schwartzbach, editors, TAPSOFT '95: Theory and Practice of Software Development, volume 915 of Lecture Notes in Computer Science, pages 262-276. Springer Verlag, 1995.

• Compositional specification and verification of distributed systems.
  B. Jonsson.
  ACM Trans. on Programming Languages and Systems, 16(2):259-303, 1994.
• A logic for reasoning about time and reliability.
  Hans Hansson and Bengt Jonsson.
  Formal Aspects of Computing 6(5):512-535, 1994.
• A fully abstract trace model for dataflow and asynchronous networks.
  B. Jonsson.
  Distributed Computing, 7:197-212, 1994.
• Decidability of timed language-inclusion for networks of real-time communicating sequential processes.
  Wang Yi and B. Jonsson.
  In Proc. 14th Conf. on Foundations of Software Technology and Theoretical Computer Science, volume 880 of Lecture Notes in G Computer Science. Springer Verlag, 1994.
• Undecidable verification problems for programs with unreliable channels.
  Parosh Aziz Abdulla and Bengt Jonsson.
  In Abiteboul and Shamir, editors, Proc. ICALP '94, volume 820 of LNCS, pages 316-327. Springer Verlag, 1994.
• Testing and refinement for nondeterministic and probabilistic processes.
  B. Jonsson, C. Ho-Stuart, and W. Yi.
  In Langmaack, de Roever, and Vytopil, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 863 of LNCS, pages 418-430. Springer Verlag, 1994.
• Using temporal logic for modular specification of telephone services.
  J. Blom, B. Jonsson, and L. Kempe.
  In L.G. Bouma and H. Velthuijsen, editors, Feature Interactions in Telecommunications Systems. IOS Press, Amsterdam, Netherlands, May 1994.
• Proving refinement using transduction.
  B. Jonsson, A. Pnueli, and C. Rump.
  Technical Report DoCS 94/54, Dept. of Computer Systems, Uppsala University, Sweden, 1994. A simultaneous technical report of Lyngby, Uppsala, and Weizmann.
  full version: postscript

• Deciding bisimulation equivalences for a class of Non-Finite-State programs.
  Bengt Jonsson and Joachim Parrow.
  Information and Computation, 107(2):272-302, December 1993.
• Validating simulations between large nondeterministic specifications.
  R. Civalero, B. Jonsson, and J. Nilsson.
  In Proc. FORTE '93. North-Holland, 1993.
• Indeterminate concurrent constraint programming: A fixpoint semantics for non-terminating computations.
  S.-O. Nyström and B. Jonsson.
  In International Logic Programming Symposium, Vancouver, British Columbia, Canada, Oct. 1993.
• Verifying programs with unreliable channels.
  Parosh Aziz Abdulla and Bengt Jonsson.
  In Proc. 8th IEEE Int. Symp. on Logic in Computer Science, pages 160-170, 1993.

• Specification and validation of a simple overtaking protocol using LOTOS.
  P. Ernberg, L.-å. Fredlund, and B. Jonsson.
  In G. Rose, editor, Proc. FORTE '91, Sydney, Australia, Nov. 1991. North-Holland.
• Towards a complete hierarchy of compositional dataflow models.
  B. Jonsson and J. Kok.
  In Proc. Int. Conf. on Theoretical Aspects of Computer Software, LNCS, Sendai, Japan, Sept. 1991. Springer Verlag.
• Simulations between specifications of distributed systems.
  B. Jonsson.
  In Proc. CONCUR '91, Theories of Concurrency: Unification and Extension, number 527 in LNCS, Amsterdam, Holland, 1991. Springer Verlag.
• Implementation of a translational semantics for an imperative language.
  L.-å. Fredlund, B. Jonsson, and J. Parrow.
  In Baeten, editor, Proc. CONCUR, Amsterdam, volume 458 of LNCS. Springer Verlag, 1990.
• Specification and refinement of probabilistic processes.
  B. Jonsson and K. Larsen.
  In Proc. 6th IEEE Int. Symp. on Logic in Computer Science, Amsterdam, Holland, July 1991.
• On the complexity of equation solving in process algebra.
  B. Jonsson and K. Larsen.
  In Abramsky and Maibaum, editors, Proc. Coll. on Trees and Algebra in Programming, volume 493 of Lecture Notes in Computer Science, pages 381-396. Springer Verlag, 1991. Extended Version as SICS Research Report 91:05.
• Refining interfaces of communicating systems. E. Brinksma, B. Jonsson, and F. Orava.
  In Abramsky and Maibaum, editors, Proc. Coll. on Combining Paradigms for Software Development, volume 494 of Lecture Notes in Computer Science, pages 297-312. Springer Verlag, 1991.

• A calculus for communicating systems with time and probabilities.
  H. Hansson and B. Jonsson.
  In Proc. 11th IEEE Real -Time Systems Symposium, Orlando, Florida, 1990.
• On decomposing and refining specifications of distributed systems.
  B. Jonsson.
  In de Bakker, de Roever, and Rozenberg, editors, Stepwise Refinement of Distributed Systems. Models, Formalisms, Correctness, volume 430 of LNCS, pages 361-385. Springer Verlag, 1990.
• A hierarchy of compositional models of I/O-automata.
  B. Jonsson.
  In Rovan, editor, Proc. Mathematical Foundations of Computer Science, volume 452 of LNCS, pages 347-354. Springer Verlag, 1990. Extended Version as SICS Research Report 91:04.
• Implementing a model checking algorithm by combining existing automated tools.
  B. Jonsson, A. Khan, and J. Parrow.
  In Sifakis, editor, Proc. Workshop on Computer Aided Verification, volume 407 of LNCS. Springer Verlag, 1990.
• Formal design of communication protocols.
  H. Hansson, B. Jonsson, F. Orava, and B. Pehrson.
  In Proc. 13th Int. Switching Symposium, Stockholm, Sweden, May 1990.

• A framework for reasoning about time and reliability.
  H. Hansson and B. Jonsson.
  In Proc. 10th IEEE Real -Time Systems Symposium, S:a Monica, Ca., 1989.
• Specification for verification.
  H. Hansson, B. Jonsson, F. Orava, and B. Pehrson.
  In Vuong, editor, Proc. FORTE, IFIP TC/WG 6.1 2nd Int. Conf. on Formal Description Techniques for Distributed Systems and Communication Protocols, pages 227 - 244, Vancouver, Canada, 1989.
• Comparing two fully abstract dataflow models.
  B. Jonsson and J. Kok.
  In Proc. PARLE '89, volume 365 of Lecture Notes in Computer Science, pages 217-234. Springer Verlag, 1989.
• Deciding bisimulation equivalences for a class of Non-Finite-State programs.
  Bengt Jonsson and Joachim Parrow.
  In Monien and Cori, editors, Proc. 6th Symposium on Theoretical Aspects of Computer Science, volume 349 of Lecture Notes in Computer Science, pages 421-433. Springer Verlag, 1989.
• A fully abstract trace model for dataflow networks.
  B. Jonsson.
  In Proc. 16th ACM Symp. on Principles of Programming Languages, pages 155-165, 1989.

• Modular verification of asynchronous networks.
  B. Jonsson.
  In Proc. 6th ACM Symp. on Principles of Distributed Computing, Vancouver, Canada, pages 152-166, Vancouver, Canada, 1987.
• Compositional Verification of Distributed Systems.
  B. Jonsson.
  PhD thesis, Dept. of Computer Systems, Uppsala University, Sweden, Uppsala, Sweden, 1987. Available as report DoCS 87/09.

• Towards deductive synthesis of dataflow networks.
  B. Jonsson, Z. Manna, and R. Waldinger.
  In Proceedings of Symposium on Logic in Computer Science, pages 26-37, 1986.

• A model and proof system for asynchronous networks.
  B. Jonsson.
  In Proc. 4th ACM Symp. on Principles of Distributed Computing, pages 49-58, Minaki, Canada, 1985.