Pest: From the lab to the classroom
Automated software verification is an active field of research which has made enormous progress both in theoretical and practical aspects. In recent years, an important effort has been put into applying these techniques on top of mainstream programming languages. These languages typically provide po...
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | , |
| Formato: | Acta de conferencia Capítulo de libro |
| Lenguaje: | Inglés |
| Publicado: |
2011
|
| Acceso en línea: | Registro en Scopus DOI Handle Registro en la Biblioteca Digital |
| Aporte de: | Registro referencial: Solicitar el recurso aquí |
| LEADER | 05119caa a22007337a 4500 | ||
|---|---|---|---|
| 001 | PAPER-10465 | ||
| 003 | AR-BaUEN | ||
| 005 | 20230518204030.0 | ||
| 008 | 190411s2011 xx ||||fo|||| 10| 0 eng|d | ||
| 024 | 7 | |2 scopus |a 2-s2.0-79959913914 | |
| 040 | |a Scopus |b spa |c AR-BaUEN |d AR-BaUEN | ||
| 030 | |a PCSED | ||
| 100 | 1 | |a De Caso, G. | |
| 245 | 1 | 0 | |a Pest: From the lab to the classroom |
| 260 | |c 2011 | ||
| 270 | 1 | 0 | |m De Caso, G.; Departamento de Computación, FCEyN, UBA, Buenos Aires, Argentina; email: gdecaso@dc.uba.ar |
| 506 | |2 openaire |e Política editorial | ||
| 504 | |a Barnett, M., Leino, K.R.M., Schulte, W., The Spec# Programming System: An Overview (2005) CASSIS, , Springer | ||
| 504 | |a Chatterjee, S., Lahiri, S.K., Qadeer, S., Rakamaric, Z., A reachability predicate for analyzing low-level software (2007) TACAS'07, pp. 19-33 | ||
| 504 | |a Cok, D.R., Kiniry, J.R., Esc/Java2: Uniting Esc/Java and JML (2005) Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, pp. 108-128 | ||
| 504 | |a De Caso, G., Gorín, D., Garbervetsky, D., Reducing the number of annotations in a verification-oriented imperative language (2009) APV'09 | ||
| 504 | |a Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R., Extended static checking for Java (2002) PLDI '02, pp. 234-245 | ||
| 504 | |a Good, D.I., London, R.L., Bledsoe, W.W., An interactive program verification system (1975) ICRE, pp. 482-492 | ||
| 504 | |a Leavens, G.T., Baker, A.L., Ruby, C., JML: A notation for detailed design (1999) Behavioral Specifications of Businesses and Systems, pp. 175-188. , Kluwer Academic Publishers | ||
| 504 | |a Leino, K.R.M., Monahan, R., Reasoning about comprehensions with first-order smt solvers (2009) SAC '09, pp. 615-622 | ||
| 504 | |a De Millo, R.A., Lipton, R.J., Perlis, A.J., Social processes and proofs of theorems and programs (1979) Commun. ACM, 22 (5), pp. 271-280 | ||
| 504 | |a Norwitz, N., PyChecker, , http://pychecker.sourceforge.net | ||
| 504 | |a Poll, E., Teaching program specification and verification using JML and ESC/Java2 (2009) TFM'09, pp. 92-104 | ||
| 504 | |a Xu, D.N., Extended static checking for Haskell (2006) SIGPLAN Workshop on Haskell, pp. 48-59A4 - ACM SIGSOFT; IEEE CS | ||
| 520 | 3 | |a Automated software verification is an active field of research which has made enormous progress both in theoretical and practical aspects. In recent years, an important effort has been put into applying these techniques on top of mainstream programming languages. These languages typically provide powerful features such as reflection, aliasing and polymorphism which are handy for practitioners but, in contrast, make verification a real challenge. The Pest programming language, on the other hand, was conceived with verifiability as one of its main design drivers. Although its main purpose is to serve as a test bed for new language features, its bare-bones syntax and strong support for annotations suggested early on in its development that it could also serve as a teaching tool for first-year undergraduate students. Developing an Eclipse plug-in for Pest proved to be both cost-effective and a key part to its adoption in the classroom. In this paper, we report on this experience. Copyright 2011 ACM. |l eng | |
| 593 | |a Departamento de Computación, FCEyN, UBA, Buenos Aires, Argentina | ||
| 690 | 1 | 0 | |a ECLIPSE PLUG-IN |
| 690 | 1 | 0 | |a LANGUAGE DESIGN |
| 690 | 1 | 0 | |a TEACHING |
| 690 | 1 | 0 | |a VERIFIABILITY |
| 690 | 1 | 0 | |a ACTIVE FIELD |
| 690 | 1 | 0 | |a ALIASING |
| 690 | 1 | 0 | |a DESIGN DRIVERS |
| 690 | 1 | 0 | |a FIRST-YEAR |
| 690 | 1 | 0 | |a KEY PARTS |
| 690 | 1 | 0 | |a LANGUAGE DESIGN |
| 690 | 1 | 0 | |a LANGUAGE FEATURES |
| 690 | 1 | 0 | |a PLUG-INS |
| 690 | 1 | 0 | |a PROGRAMMING LANGUAGE |
| 690 | 1 | 0 | |a SOFTWARE VERIFICATION |
| 690 | 1 | 0 | |a TEACHING TOOLS |
| 690 | 1 | 0 | |a UNDERGRADUATE STUDENTS |
| 690 | 1 | 0 | |a VERIFIABILITY |
| 690 | 1 | 0 | |a EQUIPMENT TESTING |
| 690 | 1 | 0 | |a SCHOOL BUILDINGS |
| 690 | 1 | 0 | |a STUDENTS |
| 690 | 1 | 0 | |a VERIFICATION |
| 690 | 1 | 0 | |a TEACHING |
| 700 | 1 | |a Garbervetsky, D. | |
| 700 | 1 | |a Gorín, D. | |
| 711 | 2 | |c Waikiki, Honolulu, HI |d 28 May 2011 through 28 May 2011 |g Código de la conferencia: 85372 | |
| 773 | 0 | |d 2011 |h pp. 5-8 |p Proc Int Conf Software Eng |n Proceedings - International Conference on Software Engineering |x 02705257 |z 9781450305990 |t 1st Workshop on Developing Tools as Plug-ins, TOPI 2011, Co-located with ICSE 2011 | |
| 856 | 4 | 1 | |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-79959913914&doi=10.1145%2f1984708.1984711&partnerID=40&md5=90bdea82ef7e0efafafabb42b8fd1cb2 |y Registro en Scopus |
| 856 | 4 | 0 | |u https://doi.org/10.1145/1984708.1984711 |y DOI |
| 856 | 4 | 0 | |u https://hdl.handle.net/20.500.12110/paper_02705257_v_n_p5_DeCaso |y Handle |
| 856 | 4 | 0 | |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_02705257_v_n_p5_DeCaso |y Registro en la Biblioteca Digital |
| 961 | |a paper_02705257_v_n_p5_DeCaso |b paper |c PE | ||
| 962 | |a info:eu-repo/semantics/conferenceObject |a info:ar-repo/semantics/documento de conferencia |b info:eu-repo/semantics/publishedVersion | ||
| 999 | |c 71418 | ||