Jaco van de Pol, Publications

1. Proceedings of the 4th International Workshop on Parallel and Distributed Methods in Verification (PDMC 2005)
   Editors: Martin Leucker and Jaco van de Pol
   In: Electronic Notes in Theoretical Computer Science, 135(2): 1-2, 2006
   
2. TTCN-3: de testtaal van de toekomst
   Joint work with: Rini van Solingen.
   In: Informatie, juli/augustus 2006.
   
3. TTCN-3 Testing of Hoorn-Kersenboogerd Railway Interlocking
   Joint work with: Jens Calame, Nicu Goga and Natalia Ioustinova.
   In: Canadian Conference on Electrical and Computer Engineering (CCECE'06)
   IEEE Press, 2006
   
4. Automatisierte Erzeugung von TTCN-3 Testfällen aus UML-Modellen
   Joint work with: Jens Calame and Natalia Ioustinova.
   In: C. Hochberger and R. Liskowsky (eds), Model-based Testing 2006 (MOTES06), Dresden, Germany, Oct 2006.
   Proc. of Informatik 2006, Lecture Notes in Informatics (LNI), pages 257-261.
   Gesellschaft für Informatik (GI), Köllen Verlag.
   
5. Simulated Time for Testing Railway Interlockings with TTCN-3
   Joint work with: Stefan Blom, Natalia Ioustinova, Axel Rennoch, Natalia Sidorova.
   In: W. Grieskamp, C. Weise (Eds.): Formal Approaches to Software Testing (FATES'05).
   LNCS 3997, Springer, pp. 1--15, 2006
   
6. Accelerated modal abstractions of labelled transition systems
   Joint work with: Miguel Valero Espada.
   In: M. Johnson, V. Vene (Eds), Algebraic Methodology And Software Technology (AMAST'06).
   LNCS 4019, Springer, pp. 338--352, 2006.
   
7. Cones and Foci: A Mechanical Framework for Protocol Verification
   Joint work with: Wan Fokkink and Jun Pang
   In: Formal Methods in System Design, 29:1--31, 2006.
   
8. Distribution of a simple shared dataspace architecture
   Joint work with Simona Orzan.
   In: Fundamenta Informaticae, 73(4):535--559, 2006.
   
9. Towards automatic generation of parameterized test cases from abstractions
   Joint work with: Jens Calame and Natalia Ioustinova.
   SEN-E0602, CWI Amsterdam, 2006
   
10. Solving scheduling problems by untimed model checking
    Joint work with: Anton Wijs and Elena Bortnik.
    Technical Report SEN-R0608, CWI Amsterdam, 2006
    
11. Bug hunting with false negatives
    Joint work with: Jens Calame, Natalia Ioustinova and Natalia Sidorova.
    Technical Report SEN-R0609, CWI Amsterdam, 2006
    
12. Integrated Formal Methods, 5th International Conference, IFM 2005
    Judi Romijn, Graeme Smith, Jaco van de Pol, editors.
    LNCS 3771, Springer, 2005.
    
13. Solving scheduling problems by untimed model checking - The Clinical Chemical Analyser Case Study
    Joint work with Anton Wijs and Elena Bortnik.
    In: Formal Methods for Industrial Critical Systems (FMICS'05)
    ACM Press, pp. 54--61, 2005.
    
14. A BDD-Representation for the Logic of Equality and Uninterpreted Functions
    Joint work with Olga Tveretina.
    In: J. Jedrzejowicz and A. Szepietowski (Eds), Mathematical Foundations of Computer Science (MFCS) 2005,
    Gdansk, Poland, Sept. 2005. LNCS 3618, Springer, pp. 769-780.
15. Generalized innermost rewriting
    Joint work with Hans Zantema.
    In: J. Giesl (ed), Proc. of 16th Int. Conf. on Rewriting Techniques and Applications
    Nara, Japan, April 2005, RTA
    LNCS , pp. 2-16, Springer
    gin.pdf
    
16. Simulated time for testing railway interlockings with TTCN-3
    Joint work with S.C.C. Blom, N. Ioustinova and N. Sidorova.
    Technical Report SEN-E0503, CWI Amsterdam, February 2005.
17. Detecting strongly connected components in large distributed state spaces
    Joint work with S.M. Orzan.
    Technical Report SEN-E0501, CWI Amsterdam, January 2005.
18. Verification of a sliding window protocol in muCRL and PVS
    Joint work with B. Badban, W. Fokkink, J.F. Groote, J. Pang.
    In: Formal Aspects of Computing 17(3): 342-388, Oct. 2005.
19. Which two-sorted algebras of Booleans and naturals have a finite basis?
    Joint work with Wan Fokkink and Sujith Vijay.
    Algebra Universalis, Vol 52(4), feb 2005, pp. 469-485.
    two-sorted.pdf
    
20. Special Section on FMICS (introductory paper)
    Joint work with Thomas Arts.
    Software Tools for Technology Transfer, Vol 7(3), 2005, pp. 195-196.
    
21. Semantic Models of a Timed Distributed Dataspace Architecture
    Joint work with Jozef Hooman.
    Theoretical Computer Science, Vol 331(2-3), 25 feb 2005, pp. 291-323.
    HoomanPolTCS.pdf
    
22. Zero, Sucessor and Equality in BDDs
    Joint work with Bahareh Badban.
    Annals of Pure and Applied Logic, Vol 133(1-3), pp. 101-123, March 2005.
    (see report version below).
    
23. Abstraction of Parallel Uniform Processes with Data
    Joint work with Jun Pang and Miguel Valero Espada.
    In: Proceedings of Software Engineering and Formal Methods (SEFM'04),
    Beijing, China, September 2004, pp. 14-23.
    sefm.pdf
24. An Abstract Interpretation Toolkit for mCRL
    Joint work with Miguel Valero Espada.
    In: Proceedings of Formal Methods in Industrial Critical Systems (FMICS'04),
    Linz, Austria, September 2004.
    Appeared in ENTCS 133, 2005, pp. 295-313.
25. A State Space Distribution Policy based on Abstract Interpretation
    Joint work with Miguel Valero Espada and Simona Orzan.
    In: Proceedings of Parallel and Distributed Methods in verifiCation (PDMC'04), London, UK, September 2004.
    Appeared in ENTCS 128(3), April 2005, pp. 35-45.
26. Modal Abstractions in mCRL
    Joint work with Miguel Valero Espada.
    In: C. Rattray, S. Maharaj and C. Shankland (eds), Proceedings of Algebraic Methodology and Software Technology (AMAST'04),
    Stirling, Scotland, July 2004, LNCS 3116, pp. 409-425.
    A full version appeared as CWI technical report SEN-R0401, February 2004, CWI, Amsterdam
    
27. Verifying a Sliding Window Protocol in mCRL
    Joint work with Wan Fokkink, Jan Friso Groote, Jun Pang and Bahareh Badban.
    In: C. Rattray, S. Maharaj and C. Shankland (eds), Proceedings of Algebraic Methodology and Software Technology (AMAST'04),
    Stirling, Scotland, July 2004, LNCS 3116, pp. 148-163.
    Full version appeared as CWI technical report SEN-R0308, September 2003, CWI, Amsterdam
    
28. Solving Satisfiability of Ground Term Algebras Using DPLL and Unification
    Joint work with Bahareh Badban, Olga Tveretina, and Hans Zantema.
    In: Proc. of Workshop on Unification, Cork, July 2004, pp. 21--36
    
29. Generalizing DPLL and Satisfiability for Equalities
    Joint work with Bahareh Badban, Olga Tveretina, and Hans Zantema.
    Technical Report SEN-R0407, CWI Amsterdam, June 2004.
30. An Algorithm to Verify Formulas by means of (0,S,=)-BDDs
    Joint work with Bahareh Badban.
    In: Proceedings of the 9th Annual Computer Society of Iran Computer Conference (CSICC 2004),
    Sharif University of Technology, Tehran, Iran, February 2004.
    confIran.pdf
    
31. Equivalent Semantic Models for a Distributed Dataspace Architecture
    Joint work with Jozef Hooman.
    In: F. de Boer, M. Bonsangue, S. Graf, W.-P. de Roever (eds), Proceedings of Formal Methods for Components and Objects (FMCO 2002, Leiden). LNCS 2852, 2003.
    
32. Verification of distributed dataspace architectures
    Joint work with Simona Orzan.
    In: Perspectives of System Informatics, Novosibirsk, Russia, July 2003.
    psi_conf.pdf, psi_full.pdf
    
33. New developments around the mCRL tool set
    Joint work with Stefan Blom, Jan Friso Groote, Izak van Langevelde and Bert Lisser.
    Thomas Arts and Wan Fokkink (eds), Proc. of FMICS 2003, Roeros, Norway.
    ENTCS (80), Elsevier Science.
    
34. Verification of JavaSpaces (TM) Parallel Programs
    Joint work with Miguel Valero Espada.
    In: J. Lilius, F. Balarin, R.J. Machado (eds), Proceedings of 3rd Int. Conf. on Application of Concurrency to System Design.
    Guimaraes, Portugal, 18-20 June 2003, (ACSD), IEEE, pp. 196-205
    ACSD_casestudy.pdf
    
35. Two Solutions to Incorporate Zero, Successor and Equality in Binary Decision Diagrams
    Joint work with Bahareh Badban.
    Technical Report SEN-R0231, December 2002, CWI, Amsterdam
    eqosbdds_report.pdf
    
36. Distribution of a simple shared dataspace architecture
    Joint work with Simona Orzan.
    In: Proc. of the 1st Int. Workshop on Foundations of Coordination Languages and Software Architectures,
    Brno, Czech Republic, August 2002, FOCLASA,
    To appear in ENTCS 68(3).
37. Refinement and verification applied to an in-flight data acquisition unit
    Joint work with Wan Fokkink, Natalia Ioustinova, Ernst Kesseler (NLR), Yaroslav Usenko Yuri Yushtein (NLR).
    In L. Brim, P. Jancar, M. Kretinsky and A. Kucera (eds), Proc. 13th Conference on Concurrency Theory,
    Brno, Czech Republic, August 2002, CONCUR,
    LNCS 2421, pp. 1-23, Springer.
    ktvfm.pdf
    
38. JITty: a Rewriter with Strategy Annotations
    In: Sophie Tison (ed), Proc. of 13th int. conf. Rewriting Techniques and Applications,
    Copenhagen, DK, July 2002, RTA System demonstration
    LNCS 2378, pp. 367-370, Springer
    jitty.pdf
    
39. State Space Reduction by Proving Confluence
    Joint work with Stefan Blom.
    In: E. Brinksma and K.G. Larsen (eds), Proc. of 14th Int. Conf. on Computer Aided Verification
    Copenhagen, DK, July 2002, CAV
    LNCS 2404, pp. 596-609, Springer
    confotf.pdf, see also the Experiments
    
40. muCRL specification of Event Notification in JavaSpaces
    Joint work with Miguel Valero Espada.
    In Proc. of X Jornadas de Concurrencia,
    Jaca, Spain, June 2002,
    pp. 191-204, Universidad de Zaragoza notify.pdf
    
41. Formal Specification of JavaSpaces Architecture using muCRL
    Joint work with Miguel Valero Espada.
    In F. Arbab and C. Talcott (eds), Proc. of 5th int. conf. on Coordination Models and Languages,
    York, UK, April 2002, COORDINATION
    LNCS 2315, pp. 274-290, Springer
    javaspaces.pdf
    
42. Formal Verification of Replication on a Distributed Data Space Architecture
    Joint work with Jozef Hooman.
    In: Proc. of ACM SAC 2002, special track on Coordination Models, Languages and Applications,
    Madrid, Spain, March 2002
    
43. Verifying Replication on a Distributed Shared Data Space with Time Stamps
    Joint work with Jozef Hooman.
    In F. Karelse (ed), Proc. of the 2nd Progress Workshop on Embedded Systems,
    Veldhoven, NL, Oct 2001,
    Published by Technology Foundation (STW), Utrecht, The Netherlands, ISBN 90-73461-27-X
    progress_2001.pdf
    
44. A Rewriting Approach to Binary Decision Diagrams
    Joint work with Hans Zantema.
    Journal of Logic and Algebraic Programming, 49(1-2):61-86,
    September 2001
    
45. mCRL: a Toolset for Analysing Algebraic Specifications
    Joint work with Stefan Blom, Wan Fokkink, Jan Friso Groote, Izak van Langevelde and Bert Lisser.
    In: Proc. of 13th INt. Conf. on Computer Aided Verification,
    Paris, France, 2001, CAV system demo
    mCRLtoolset.pdf
    
46. Just-in-time: On Strategy Annotations
    Int. Workshop on Reduction Strategies in Rewriting and Programming (WRS 2001).
    Electronic Notes in Theoretical Computer Science, Elseviers, Volume 57.
    (available as Technical Report SEN-R0105, CWI, Amsterdam)
    
47. Expressiveness of Basic Splice
    Technical Report SEN-R0033, CWI, Amsterdam
    splice.pdf
    
48. State Space Reduction using Partial $\tau$-Confluence
    Joint work with Jan Friso Groote.
    (MFCS 2000, Bratislava, LNCS 1893, pp. 383-393)
    locconf.pdf
    
49. Equational Binary Decision Diagrams
    Joint work with Jan Friso Groote.
    (LPAR 2000, Reunion Island, LNAI 1955, pp. 161-178)
    eqbdds.pdf
    
50. Binary Decision Diagrams by Shared Rewriting
    Joint work with Hans Zantema.
    (MFCS 2000, Bratislava, LNCS 1893, pp. 609-618)
    mfcs_bdd.pdf
    
51. Requirements Specification and Analysis of Command and Control Systems
    Joint work with Jozef Hooman and Edwin de Jong
    Technical Report 99-09, Computer Science Reports, Eindhoven Univerisity of Technology
    orkest.pdf
52. Modular Formal Specification of Data and Behaviour
    Joint work with Jozef Hooman and Edwin de Jong
    (IFM'99, York, UK)
    mfsdb.pdf
53. Checking Verifications of Protocols and Distributed Systems by Computer
    Joint work with Jan Friso Groote and Francois Monin.
    (CONCUR '98, Nice, LNCS 1466, pp. 629-655)
    Extended version: concur.pdf
54. Formal Requirements Specification for Command and Control Systems
    Joint work with Jozef Hooman and Edwin de Jong
    (ECBS 1998, Jerusalem)
    ecbs.pdf
55. Simulation as a Correct Transformation of Rewrite Systems
    Joint work with Wan Fokkink
    (MFCS 1997, published in LNCS 1295)
    mfcs.pdf
    (Full version available in Utrecht's Logic Group Preprint Series, No. 164, 1996)
    transformation.pdf
    
56. Termination of Higher-order Rewrite Systems
    (Manuscript of my PhD thesis, august 1996)
    thesis.pdf
57. Operational Semantics of Rewriting with Priorities
    Published in Theoretical Computer Science 200(1-2), pp. 289-312.
    Preprint available in: Utrecht's Logic Group Preprint Series, No. 162, 1996.
    prs.pdf
    
58. A Calculus for Sequential Logic with 4 Values
    Joint work with Jan A. Bergstra
    Available in Utrecht's Logic Group Preprint Series, No. 160, 1996.
    fourvalued.pdf
    
59. Two Different Strong Normalization Proofs?
    - computability versus functionals of finite type -
    (HOA 1995, published in LNCS 1074)
    different.pdf.
60. A Bounded Retransmission Protocol for Large Data Packets
    - a case study in computer checked algebraic verification -
    Joint work with Jan Friso Groote
    (AMAST 1996, published in LNCS 1101)
    brp.pdf.
    (An obscure version is available in Utrecht's Logic Group Preprint Series, No. 100, 1993)
61. Strict Functionals for Termination Proofs
    Joint work with Helmut Schwichtenberg
    (TLCA 1995, published in LNCS 902)
    strict.pdf.
62. Termination Proofs for Higher-order Rewrite Systems
    (HOA 1993, published in LNCS 816)
    termination.pdf.
63. Modularity in Many-sorted Term Rewriting Systems
    (Master's thesis, 1992)
    modularity.pdf

Back to Homepage

Jaco van de Pol