Aleksandar S. Dimovski

Office: 4D04

Email: adim@itu.dk

Phone: +45 7652 2412

 

 

 

Software & Systems Group

IT University of Copenhagen

 

 

 

 


  Home

  Research

  Publications

  CV





 

Research:

My research is currently focused on verification single programs and program families using combination of techniques like Model Checking, Static Program Analysis, Abstract Interpretation, and Game Semantics.

Keywords: Software model checking, Static program analysis, Abstract interpretation, Game semantics, Process algebra.

Tools:

Committees: SPIN'16, SPLat'15, SPLat'14

 

PhD Thesis:

  • A. Dimovski. Compositional Software Verification Based on Game Semantics. PhD Thesis, University of Warwick, UK, July 2007. (PDF)

Journals:

  • A. S. Dimovski, A. S. Al-Sibahi, C. Brabrand, A. Wasowski. Efficient family-based model checking via variability abstractions. In International Journal on Software Tools for Technology Transfer (STTT), Vol. : 1-19, Springer-Verlag, 2016. (PDF)

  • J. Midtgaard, A. S. Dimovski, C. Brabrand, A. Wasowski. Systematic derivation of correct variability-aware program analyses. In Science of Computer Programming (SCP), Vol. 105: 145-170, Elsevier, 2015. (PDF)

  • A. S. Dimovski. Program verification using symbolic game semantics. In Theoretical Computer Science (TCS), Vol. 560: 364-379, Elsevier, 2014. (PDF)

  • A.Bakewell, A. Dimovski, D. R. Ghica, and R. Lazic. Data-abstraction refinement: a game semantic approach. In International Journal on Software Tools for Technology Transfer (STTT), Vol. 12(5): 373--389, Springer-Verlag, 2010. (PDF)

  • A. Dimovski and R. Lazic. Compositional  software verification based on game semantics and process algebra. In International Journal on Software Tools for Technology Transfer (STTT), Vol. 9(1): 37--51, Springer-Verlag, 2007. (PDF)

Conferences:

  • A. S. Dimovski. Symbolic Game Semantics for Model Checking Program Families. In Proceedings of the 23rd International SPIN Symposium on Model Checking of Software (SPIN 2016), Lecture Notes in Computer Science 9641: 19-37, Springer, Eindhoven, April 2016. (PDF).

  • A. S. Dimovski, C. Brabrand, A. Wasowski. Variability Abstractions: Trading Precision for Speed in Family-Based Analyses. In Proceedings of the 29th European Conference on Object-Oriented Programming (ECOOP'15), LIPIcs 37: 247-270, Prague, July 2015. (PDF)

  • A. S. Dimovski, A. S. Al-Sibahi, C. Brabrand, A. Wasowski. Family-Based Model Checking without a Family-Based Model Checker. In Proceedings of the 22nd International SPIN Symposium on Model Checking of Software (SPIN 2015), Lecture Notes in Computer Science 9232: 282-299, Springer, Stellenbosch, August 2015. (PDF)

  • A. F. Iosif-Lazar, A. S. Al-Sibahi, A. S. Dimovski, J. E. Savolainen, K. Sierszecki, A. Wasowski. Experiences from Designing and Validating a Software Modernization Transformation. In Proceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering (ASE '15), IEEE 2015: 597-607, Lincoln, November 2015. (PDF)

  • A. S. Dimovski. Ensuring Secure Non-interference of Programs by Game Semantics. In Proceedings of the 10th International Workshop on Security and Trust Management (STM'14), Lecture Notes in Computer Science 8743: 81-96, Springer, Wroclaw, September 2014. (PDF)

  • A. S. Dimovski. Slot Games for Detecting Timing Leaks of Programs. In Proceedings of the 4th International Symposium on Games, Automata, Logics and Formal Verification (GandALF'13), Electronic Proceedings in Theoretical Computer Science 119: 166-179, Borca di Cadore, August 2013. (PDF)

  • A. S. Dimovski. Verifying Data Independent Programs Using Game Semantics. In Proceedings of the 12th International Conference on Software Composition (SC'13), Lecture Notes in Computer Science 8088: 128-143, Springer, Budapest, June 2013. (PDF)

  • A. S. Dimovski. Symbolic Representation of Algorithmic Game Semantics. In Proceedings of the 3rd International Symposium on Games, Automata, Logics and Formal Verification (GandALF'12), Electronic Proceedings in Theoretical Computer Science 96: 99-112, Naples, September 2012. (PDF)

  • A. S. Dimovski. Parameterized Verification of Open Procedural Programs. In Proceedings of the 5th Balcan Conference in Informatics (BCI'12), ACM ICPS series: 180-185, Novi Sad, September 2012. (PDF)

  • A. S. Dimovski. A Compositional Method for Deciding Equivalence and Termination of Nondeterministic Programs. In Proceedings of the 8th International Conference on Integrated Formal Methods (iFM'10), Lecture Notes in Computer Science 6396: 121-135, Springer, Nancy, October 2010. (PDF)

  • A. S. Dimovski, G. Velinov, and D. Sahpaski. Horizontal Partitioning by Predicate Abstraction and its Application to Data Warehouse Design. In Proceedings of the 14th East European Conference on Advances in Databases and Information Systems (ADBIS'10), Lecture Notes in Computer Science 6295: 164-175, Springer, Novi Sad, September 2010. (PDF)

  • A. Dimovski and R. Lazic. Assume-Guarantee Software Verification Based on Game Semantics. In Proceedings of the 8th International Conference on Formal Engineering Methods (ICFEM'06), Lecture Notes in Computer Science 4260: 529-548, Springer, Macao, November 2006. (PDF)

  • A. Dimovski, D. R. Ghica and R. Lazic. A Counterexample-Guided Refinement Tool for Open Procedural Programs. In Proceedings of the 13th International SPIN Workshop on Model Checking of Software (SPIN'06), Lecture Notes in Computer Science 3925: 288-292,  Springer, Vienna, March 2006. (PDF)

  • A. Dimovski, D. R. Ghica and R. Lazic. Data-Abstraction Refinement: A Game Semantic Approach. In Proceedings of the 12th International Static Analysis Symposium (SAS'05), Lecture Notes in Computer Science 3672: 102-117,  Springer, London, September 2005. (PDF)

  • A. Dimovski and R. Lazic. Software Model Checking Based on Game Semantics and CSP. In Proceedings of the 4th International Workshop on Automated Verification of Critical Systems (AVoCS'04), Electronic Notes in Theoretical Computer Science 128(6): 105-125, Elsevier, London, September 2004. (PDF)

  • Dimovski and R. Lazic. CSP Representation of Game Semantics for Second-order Idealized Algol. In Proceedings of the 6th International Conference on Formal Engineering Methods (ICFEM'04), Lecture Notes in Computer Science 3308: 146-161, Springer, Seattle, November 2004. (PDF)

  • A. Dimovski and D. Gligoroski. Generating highly nonlinear Boolean functions using a Genetic algorithm. In Proceedings of 1st Balcan Conference in Informatics (BCI'03), Thessaloniki, Greece, November 2003. (PDF)