Breadcrumb

 
 

Formally Specifying and Proving Operational Aspects of Forensic Lucid in Isabelle

Title:

Formally Specifying and Proving Operational Aspects of Forensic Lucid in Isabelle

Mokhov, Serguei A. and Paquet, Joey (2008) Formally Specifying and Proving Operational Aspects of Forensic Lucid in Isabelle. In: 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs) 2008, Emerging Trends Proceedings, August 2008, Montreal, QC, Canada.

[img]
Preview
PDF - Published Version
253Kb

Official URL: http://users.encs.concordia.ca/~tphols08/TPHOLs200...

Abstract

A Forensic Lucid intensional programming language has been proposed for intensional cyberforensic analysis. In large part, the language is based on various predecessor and codecessor Lucid dialects bound by the higher-order intensional logic (HOIL) that is behind them. This work formally specifies the operational aspects of the Forensic Lucid language and compiles a theory of its constructs using Isabelle, a proof assistant system.

Divisions:Concordia University > Faculty of Engineering and Computer Science > Computer Science and Software Engineering
Item Type:Conference or Workshop Item (Poster)
Refereed:Yes
Authors:Mokhov, Serguei A. and Paquet, Joey
Date:August 2008
Projects:
  • Forensic Lucid
  • General Intensional Programming System
Funders:
  • Faculty of Engineering and Computer Science, Concordia, Canada
  • NSERC
Keywords:Forensic Lucid, Isabelle, General Intensional Programming System (GIPSY), higher-order intensional logic (HOIL), digital forensics, forensic computing, programming languages, specification languages, context-aware computing
ID Code:15113
Deposited By:Serguei Mokhov
Deposited On:30 Sep 2011 11:09
Last Modified:30 Sep 2011 11:09
Related URLs:
Additional Information:Part of the ConU technical report "2008-1-Ait Mohamed" found at http://users.encs.concordia.ca/~tphols08/TPHOLs2008/ET/EmergingTrends08.pdf
References:
1. Mokhov, S.: Intensional Forensics – the Use of Intensional Logic in Cyberforensics. Technical report, Concordia Institute for Information Systems Engineering, Concordia University, Montreal, Canada (January 2007) ENGR6991 Technical Report.

2. Mokhov, S.: Intensional Cyberforensics – a PhD Proposal. Department of Computer Science and Software Engineering,
Concordia University, Montreal, Canada (December 2007)

3. The GIPSY Research and Development Group: The General Intensional Programming System (GIPSY) project. Department
of Computer Science and Software Engineering, Concordia University, Montreal, Canada (2002-2008) http://newton.cs.
concordia.ca/~gipsy/, last viewed April 2008.

4. Paulson, L.C., Nipkow, T.: Isabelle: A generic proof assistant. University of Cambridge and Technical University of Munich (2007) http://isabelle.in.tum.de/, last viewed: December 2007.

5. Wadge, W., Ashcroft, E.: Lucid, the Dataflow Programming Language. Academic Press, London (1985)

6. Edward Ashcroft and Anthony Faustini and Raganswamy Jagannathan and William Wadge: Multidimensional, Declarative
Programming. Oxford University Press, London (1995)

7. Ashcroft, E.A., Wadge, W.W.: Lucid - A Formal System for Writing and Proving Programs. Volume 5., SIAM J. Comput. no.
3 (1976)

8. Ashcroft, E.A.,Wadge,W.W.: Erratum: Lucid - A Formal System for Writing and Proving Programs. Volume 6(1):200., SIAM J. Comput. (1977)

9. Ashcroft, E.A., Wadge, W.W.: Lucid, a nonprocedural language with iteration. Communication of the ACM 20(7) (July 1977) 519–526

10. Gagn´e, J.R., Plaice, J.: Demand-Driven Real-Time Computing, World Scientific (September 1999)

11. Paquet, J.: Scientific Intensional Programming. PhD thesis, Department of Computer Science, Laval University, Sainte-Foy, Canada (1999)

12. Wan, K., Alagar, V., Paquet, J.: A Context theory for Intensional Programming. In: Workshop on Context Representation and Reasoning (CRR05), Paris, France. (July 2005)

13. Wan, K.: Lucx: Lucid Enriched with Context. PhD thesis, Department of Computer Science and Software Engineering,
Concordia University, Montreal, Canada (2006)

14. Paquet, J., Mokhov, S.A., Tong, X.: Design and implementation of context calculus in the GIPSY environment. In: Proceedings of the 32nd Annual IEEE International Computer Software and Applications Conference (COMPSAC), Turku, Finland, IEEE Computer Society (July 2008) 1278–1283

15. Tong, X.: Design and implementation of context calculus in the GIPSY. Master’s thesis, Department of Computer Science and Software Engineering, Concordia University, Montreal, Canada (April 2008)

16. Wan, K., Alagar, V., Paquet, J.: Lucx: Lucid Enriched with Context. In: Proceedings of the 2005 International Conference on Programming Languages and Compilers (PLC 2005), Las Vegas, USA, CSREA Press (June 2005) 48–14

17. Mokhov, S.A.: Towards syntax and semantics of hierarchical contexts in multimedia processing applications using MARFL. In: Proceedings of the 32nd Annual IEEE International Computer Software and Applications Conference (COMPSAC), Turku, Finland, IEEE Computer Society (July 2008) 1288–1294

18. Swoboda, P.: A Formalisation and Implementation of Distributed Intensional Programming. PhD thesis, The University of New South Wales, Sydney, Australia (2004)

19. Swoboda, P., Wadge, W.W.: Vmake, ISE, and IRCS: General tools for the intensionalization of software systems. In Gergatsoulis, M., Rondogiannis, P., eds.: Intensional Programming II, World-Scientific (2000)

20. Swoboda, P., Plaice, J.: A new approach to distributed context-aware computing. In Ferscha, A., Hoertner, H., Kotsis, G., eds.: Advances in Pervasive Computing, Austrian Computer Society (2004) ISBN 3-85403-176-9.

21. Swoboda, P., Plaice, J.: An active functional intensional database. In Galindo, F., ed.: Advances in Pervasive Computing, Springer (2004) 56–65 LNCS 3180.

22. Gladyshev, P., Patel, A.: Finite state machine approach to digital event reconstruction. In: Digital Investigation Journal. Volume 2. (2004)

23. Gladyshev, P.: Finite state machine analysis of a blackmail investigation. In: International Journal of Digital Evidence, Technical and Security Risk Services, Sprint 2005, Volume 4, Issue 1 (2005)

24. Ding, Y.M.: Bi-directional translation between data-flow graphs and Lucid programs in the GIPSY environment. Master’s thesis, Department of Computer Science and Software Engineering, Concordia University, Montreal, Canada (2004)

25. Tong, X., Paquet, J., Mokhov, S.A.: Context Calculus in the GIPSY. Unpublished (2007)

26. Mokhov, S.A., Paquet, J., Debbabi, M.: Designing a language for intensional cyberforensic analysis. Unpublished (2007)

27. Klein, G., Nipkow, T., Paulson, L.C.: The archive of formal proofs. SourceForge.net (2008) http://afp.sourceforge.net/, last viewed: April 2008.

28. Moeller, A.: Program Verification with Hoare Logic. Technical report, University of Aarhus (2004) http://www.brics.dk/~amoeller/talks/hoare.pdf.

29. Mokhov, S.A., Paquet, J., Tong, X.: Hybrid intensional-imperative type system for intensional logic support in GIPSY. Submitted for publication at LPAR’08 (2008)

30. Shafer, G.: The Mathematical Theory of Evidence. Princeton University Press (1976)

31. Haenni, R., Kohlas, J., Lehmann, N.: Probabilistic argumentation systems. Technical report, Institute of Informatics, University of Fribourg, Fribourg, Switzerland (October 1999)

32. Kahn, G.: The semantics of a simple language for parallel processing. In: Proceedings of the IFIP Congress ’74, Amsterdam, Elsevier North-Holland (1974) 471–475

33. Kahn, G., MacQueen, D.B.: Coroutines and networks of parallel processes. In: Proceedings of the IFIP Congress ’77, Amsterdam, Elsevier North-Holland (1977) 993–998
34. Landin, P.J.: The next 700 programming languages. Communications of the ACM 9(3) (1966) 157–166
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Document Downloads

More statistics for this item...

Concordia University - Footer