Email:

aleksandar.dimovski@unt.edu.mk

  Home

  Research

  Publications

  CV

My research is currently focused on analyzing/verifying 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:

• GameChecker - Verification Tool based on Game Semantics and CSP

• Symbolic GameChecker - Verification Tool based on Symbolic Game Semantics

Publications:

PhD Thesis:

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

Journals:

• A. S. Dimovski. Fault localization by abstract interpretation and its applications. In In Journal of Computer Languages (COLA), Vol. 80: 101288, Elsevier, 2024. (PDF)

• A. S. Dimovski,S. Apel, and A. Legay. Quantitative program sketching using decision tree-based lifted analysis. In In Journal of Computer Languages (COLA), Vol. 75: 101206, Elsevier, 2023. (PDF)

• A. S. Dimovski,S. Apel, and A. Legay. Synthesizing PROMELA model sketches using abstract lifted model checking. In In International Journal of Information Technology, Vol. 16(1): 425–435, Springer, 2024. (PDF)

• A. S. Dimovski,S. Apel, and A. Legay. Several Lifted Abstract Domains for Static Analysis of Numerical Program Families. In In Science of Computer Programming (SCP), Vol. 213: 102725, Elsevier, 2022. (PDF)

• A. S. Dimovski. A binary decision diagram lifted domain for analyzing program families. In Journal of Computer Languages (COLA), Vol. 63: 101032, Elsevier, 2021. (PDF)

• A. S. Al-Sibahi, T. P. Jensen, A. Dimovski, A. Wasowski. Verification of program transformations with inductive refinement types. In ACM Transactions on Software Engineering and Methodology (TOSEM), Vol. 30(1): 5:1--5:33, ACM, 2021. (PDF)

• A. Dimovski, A. Legay, A. Wasowski. Generalized abstraction-refinement for game-based CTL lifted model checking. In Theoretical Computer Science (TCS), Vol. 837: 181--206, Elsevier, 2020. (PDF)

• A. S. Dimovski. On calculating assertion probabilities for program families. In PRILOZI CONTRIBUTIONS, Sec. Nat. Math. Biotech. Sci, MASA, Vol. 41(1): 13--23, MASA, 2020. (PDF)

• A. S. Dimovski. CTL* family-based model checking using variability abstractions and modal transition systems. In International Journal on Software Tools for Technology Transfer (STTT), Vol. 22(1): 35--55 , Springer-Verlag, 2019. (PDF)

• A. S. Dimovski, C. Brabrand, A. Wasowski. Finding suitable variability abstractions for lifted analysis. In Formal Asp. Comput., (FAOC), Vol. 31(2) : 231-259, Springer, 2019. (PDF)

• A. S. Dimovski, C. Brabrand, A. Wasowski. Variability abstractions for lifted analyses. In Science of Computer Programming (SCP), Vol. 159 : 1-27, Elsevier, 2018. (PDF)

• A. S. Dimovski. Verifying annotated program families using symbolic game semantics. In Theoretical Computer Science (TCS), Vol. 706 : 35-53, Elsevier, 2018.(PDF)

• B. Atanasovski, M. Bogdanovic, G. Velinov, L. Stoimenov, A. Dimovski, B. Koteska, D. Jankovic, I. Skrceska, M. Kon-Popovska, B. Jakimovski. On defining a model driven architecture for an enterprise e-health system. In Enterprise Information Systems (EIS), Vol. 12(8-9): 915-941, Taylor \& Francis Online, 2018 (PDF)

• A. F. Iosif-Lazar, J. Melo, A. S. Dimovski, C. Brabrand, A. Wasowski. Effective Analysis of C Programs by Rewriting Variability. In The Art, Science, and Engineering of Programming Journal (Programming Journal), Vol. 1(1): 1-25, , 2017. (PDF)

• 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. 19(5): 585-603, 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. Generalized Program Sketching by Abstract Interpretation and Logical Abduction. In Proceedings of the 30th International Symposium on Static Analysis (SAS 2023), Lecture Notes in Computer Science 14284: 212--230, Springer, Cascais, Portugal, October 22-24, 2023. (preprint PDF).

A. S. Dimovski. Error Invariants for Fault Localization via Abstract Interpretation. In Proceedings of the 30th International Symposium on Static Analysis (SAS 2023), Lecture Notes in Computer Science 14284: 190--211, Springer, Cascais, Portugal, October 22-24, 2023. (preprint PDF).

• A. S. Dimovski, S. Lazreg, M. Cordy, A. Legay. . Family-based model checking of fMultiLTL properties. In Proceedings of the 27th ACM International Systems and Software Product Line Conference - Volume A (SPLC 2023), ACM, Tokyo, Japan, 28 August 2023. (preprint PDF).

• A. S. Dimovski. Quantitative Program Sketching using Lifted Static Analysis. In Proceedings of the 25th International Conference on Fundamental Approaches to Software Engineering (FASE 2022), Lecture Notes in Computer Science 13241: 102--122, Springer, Munich, Germany, April 2-7, April 2021. (preprint PDF).

• A. S. Dimovski. Lifted Termination Analysis by Abstract Interpretation and Its Applications. In Proceedings of the 20th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences (GPCE 2021), , ACM, Chicago, USA, October, 2021. (preprint PDF).

• A. S. Dimovski, S. Apel. Lifted Static Analysis of Dynamic Program Families by Abstract Interpretation. In Proceedings of the 35th European Conference on Object-Oriented Programming (ECOOP'21), LIPIcs 194: 14:1--14:28, Aarhus (Virtual Conference), July 2021. (PDF)

• A. Dimovski, S. Apel, A. Legay. Program Sketching Using Lifted Analysis for Numerical Program Families. In Proceedings of the 13th International Symposium NASA Formal Methods (NFM'21), Lecture Notes in Computer Science 12673: 95--112, Springer, Virtual Event, May 2021. (preprint PDF).

• A. Dimovski, S. Apel, A. Legay. A Decision Tree Lifted Domain for Analyzing Program Families with Numerical Features. In Proceedings of the 24th International Conference on Fundamental Approaches to Software Engineering (FASE 2021), Lecture Notes in Computer Science 12649: 67--86, Springer, Luxembourg, April 2021. (preprint PDF).

• A. S. Dimovski, A. Legay. Computing Program Reliability Using Forward-Backward Precondition Analysis and Model Counting. In Proceedings of the 23rd International Conference on Fundamental Approaches to Software Engineering (FASE 2020), Lecture Notes in Computer Science 12076: 182--202, Springer, Dublin, April 2020. (preprint PDF).

• A. S. Dimovski. Lifted Static Analysis using a Binary Decision Diagram Abstract Domain. In Proceedings of the 18th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences (GPCE 2019), 102--114, ACM, Athens, Greece, October, 2019. (preprint PDF).

• A. S. Dimovski, A. Legay, A. Wasowski. Variability Abstraction and Refinement for Game-Based Lifted Model Checking of Full CTL. In Proceedings of the 22nd International Conference on Fundamental Approaches to Software Engineering (FASE 2019), Lecture Notes in Computer Science 11424: 192--209, Springer, Prague, April 2019. (preprint PDF).

• A. S. Al-Sibahi, T. P. Jensen, A. S. Dimovski, A. Wasowski. Verification of high-level transformations with inductive refinement types. In Proceedings of the 17th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences (GPCE 2018), 147--160, ACM, Boston, MA, USA, November, 2018. [best paper award] (preprint PDF).

• A. S. Dimovski. Abstract Family-based Model Checking using Modal Featured Transition Systems: Preservation of CTL*. In Proceedings of the 21st International Conference on Fundamental Approaches to Software Engineering (FASE 2018), Lecture Notes in Computer Science 10802: 301--318, Springer, Thessaloniki, April 2018. (preprint PDF).

• A. S. Dimovski. Probabilistic Analysis Based On Symbolic Game Semantics and Model Counting. In Proceedings of the 8th International Symposium on Games, Automata, Logics and Formal Verification (GandALF'17), Electronic Proceedings in Theoretical Computer Science 256: 1-15, Rome, September 2017. (preprint PDF).

• A. S. Dimovski, A. Wasowski. Variability-specific Abstraction Refinement for Family-based Model Checking. In Proceedings of the 20th International Conference on Fundamental Approaches to Software Engineering (FASE 2017), Lecture Notes in Computer Science 10202: 406--423, Springer, Uppsala, April 2017. (preprint PDF).

• A. S. Dimovski, A. Wasowski. From Transition Systems to Variability Models & From Lifted Model Checking Back to UPPAAL. In Proceedings of Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday (KiMfest 2017), Lecture Notes in Computer Science 10460: 249--268, Springer, Aalborg, August 2017. (preprint PDF).

• A. S. Dimovski, C. Brabrand, A. Wasowski. Finding Suitable Variability Abstractions for Family-Based Analysis. In Proceedings of the 21st International Symposium on Formal Methods (FM 2016), Lecture Notes in Computer Science 9995: 217-234, Springer, Limassol, November 2016. (PDF).

• 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. Al-Sibahi, A. S. Dimovski, A. Wasowski. Symbolic Execution of High-level Transformations. In Proceedings of the 2016 ACM SIGPLAN International Conference on Software Language Engineering (SLE 2016), ACM: 207-220, Amsterdam, October 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)