Solving contest problems via formal program verification

N.V. Shilov, S.O. Shilova

Abstract


The interface between mathematics and computer science is many-sided. In particular, E.W. Dijkstra promoted a special “computer science” approach to mathematics problem solving. The approach combines a heuristic algorithm design and rigorous mathematical proof of algorithm correctness (in style of A. Hoare and R. Floyd). The paper sketches two problems of this kind in a form of tutorials for undergraduate students that are interested in different programming contests (like ACM International Collegiate Programming Contests). These tutorials took place at Novosibirsk State University in years 2005–2008. The paper also dioceses some direction for further research that emerge from the problems.
Problems in programming 2010; 2-3:355-362

Full Text:

PDF

References


K.R. Apt, F.S. de Boer and E.R. Olderog. Verification of Sequential and Concurrent Programs, 3rd ed., Springer-Verlag, 2009.

E.V. Bodin, L.V. Gorodnjay, N.V. Shilov. What is the subject of the computer science contest? Preprint #126, A.P. Ershov Institute of Informatics Systems, Novosibirsk, 2005 (in Russian).

R. Burkard, M. Dell'Amico, S. Martello. Assignment Problems. SIAM, 2009.

E.W. Dijkstra. On a cultural gap. The Mathematical Intelligencer, 8(1), 1986. – Р. 48–52.

R.W. Floyd. Assigning Meanings to Programs, in Mathematical Aspects of Computer Science (Proc. of Symp. in Applied Mathematics), 1967, vol. 19. – Р. 19–32.

C.A.R. Hoare. The Verifying Compiler: A Grand Challenge for Computing Research, in Lecture Notes in Computer Science (Proc. of Conf. "Perspectives of System Informatics" (PSI 2003)), 2003, vol. 2890. – Р. 103–111.

O. Hazzan. Application of computer science ideas to the presentation of mathematical theorems and proofs. ACM SIGCSE Bull., 35(2), 2003. – Р. 38–42.

J. Hershberger and S. Suri. Applications of a semi-dynamic convex hull algorithm. Proc. of the 2nd Scandinavian Workshop on Algorithm

Theory SWAT’90, Lecture Notes in computer Science, v. 447, Springer-Verlag, 1990. – Р. 380–392.

J. Malkevitch. A Discrete Geometrical Gem. AMS Feature Column Monthly Essays on Mathematical Topic. July-August, 2003,

http://www.ams.org/featurecolumn/archive/index.html.

J. Pach, P. Agarwal. Combinatorial Geometry. Wiley-Interscience 1995.

N. Shilov and K. Yi. Engaging Students with Theory through ACM Collegiate Programming Contests. Communications of ACM. – v. 45,

N 9. – 2002.

N.V. Shilov, S.O. Shilova. Etude on theme of Dijkstra. ACM SIGACT News, 35(3), 2004. – Р. 102–108.

N.V. Shilov, S.O. Shilova. On Mathematical Contents of Computer Science Contests. Proceedings of the 1st KAIST International Symposium on Enhancing University Mathematics Teaching, 12–16 May, Daejeon, Korea. – 2005. – Р. 223–233.

N.V. Shilov, N.O. Garanina. Modal Logics for reasoning about Multiagent Systems. In Encyclopedia of Artificial Intelligence. J.R. Rabucal, J. Dorado, A.P. Sierra, editors. Information Science Reference. 2008. – Р. 1089–1094.

N.O. Garanina, N.V. Shilov and L.E. Konyaev. Can Robots Solve the Assignment Problem? Proceedings of the 2009 Workshop on

Concurrency, Specification, and Programming. Kraków–Przegorzały, Poland, 28–30 September 2009, v. 1. – 2009. – Р. 154–163.

G. Tel Introduction to Distributed Algorithms. Cambridge University Press, 2nd Edition, 2000.

M. Wooldridge. An Introduction to Multiagent Systems. John Willey & Sons Ltd, 2002.


Refbacks

  • There are currently no refbacks.