The ACM/IEEE-CS Computer Science Curricula 2013 (CS2013) report provides guidelines on undergraduate programs in computer science. The report includes a knowledge area on Intelligent Systems, which presents the topics and learning outcomes related to AI that are recommended for undergraduate CS programs to include.

For over 40 years, the ACM and IEEE-Computer Society have sponsored international curricular guidelines for undergraduate programs in computing. The rapid evolution and expansion of the computing field and the growing number of topics in computer science have made regular revision of curricular recommendations necessary. Thus, the Computing Curricula volumes are updated on an approximately 10-year cycle, with the aim of keeping curricula modern and relevant. The latest volume in the series, Computer Science Curricula 2013 (CS2013), is due for release in the Fall of 2013. This panel seeks to inform the SIGCSE community about the final version of the report, provide insight on interpreting the CS2013 guidelines, and give guidance regarding how the guidelines may be implemented at different institutions.

center in Ankara. After the tour ended, the minibus driver started driving us back to the conference center. However, Barbara had other plans for all of us. She talked the driver into stopping the bus by the side of the road to look for a particular geocache. He didn't really understand what we were looking for, but she had him and everyone on the tour walking around looking for it. I don't think we ever found it. " Henry Walker, Grinnell College, writes: " One element of being SIGCSE Chair (or past Chair) is that one must be ready for almost anything—often without warning. As an example, the ITiCSE 2011 conference dinner in Darmstadt, Germany, included entertainments that involved various skits. The final skit was substantially longer and more involved than the others. It turned out that the conference leaders had arranged with the dinner hosts to select Barbara and me to be "Queen" and "Knight" in a lengthy story. " Thank you, Barb. Your leadership on the Board will be missed. For over 40 years, the major professional societies in computing—ACM and IEEE-Computer Society—have sponsored the creation of international curricular guidelines for undergraduate programs in computing. As the field has grown and diversified, so too have the recommendations for curricula. The rapid evolution and expansion of the computing field and the growing number of topics in computer science has made regular revision of curricular recommendations necessary. Thus, the Computing Curricula volumes are updated on an approximately 10-year cycle, with the aim of keeping curricula modern and relevant. The most recent complete Computer Science curricular volume was released in 2001 (CC2001) and was followed by a review effort that concluded in 2008 (CS2008). The next volume in the series, Computer Science Curricula 2013 (CS2013), is currently in progress, and two drafts of the CS2013 report have already been released—the Strawman draft in February 2012 and the Ironman draft in February 2013. The final CS2013 report will be released by the end of this calendar year. CS2013 aims to provide advice and guidance to the computing education community throughout the coming decade by redefining the knowledge areas in CS, rethinking the essentials necessary for a CS curriculum, and identifying actual fielded exemplary courses and curricula along these lines. Balancing topical growth with the need to keep recommendations realistic and implementable in the context of undergraduate education is particularly challenging. Further, the …

ABSTRACTFor over 40 years, the ACM and IEEE-Computer Society have sponsored the creation of international curricular guidelines for undergraduate programs in computing. These Computing Curricula volumes are updated approximately every 10-year cycle, with the aim of keeping curricula modern and relevant. The next volume in the series, Computer Science 2013 (CS2013), is currently in progress. This panel seeks to update and engage the SIGCSE community in providing feedback on a complete draft of the CS2013 report (called the Ironman report), which will be released shortly before SIGCSE. Since the Ironman report is the penultimate draft of the CS2013 report, this panel is an especially important venue for starting the last round of feedback that will impact the final CS2013 curricular guidelines.

Beginning with the publication of Curriculum 68, ACM and IEEE-Computer Society have sponsored various efforts to establish international curricular guidelines for undergraduate programs in computing. Work on the next volume, Computer Science 2013 is well underway, with the Ironman draft out shortly before SIGCSE 2013. The Ironman draft includes course and curricular exemplars, which should serve as a rich resource for those trying to meet the curriculum standards. This special session highlights the exemplar section of the Ironman report through a description of its purpose, presentation of several exemplars, and an invitation to the SIGCSE community to participate by submitting exemplars and providing feedback on what they would find useful in this section of the CS 2013 final report.

Beginning over 40 years ago with the publication of Curriculum 68, the major professional societies in computing--ACM and IEEE-Computer Society--have sponsored various efforts to establish international curricular guidelines for undergraduate programs in computing. As the field has grown and diversified, so too have the recommendations for curricula. There are now guidelines for Computer Engineering, Information Systems, Information Technology, and Software Engineering in addition to Computer Science. These volumes are updated regularly with the aim of keeping computing curricula modern and relevant. In the Fall of 2010, work on the next volume in the series, Computer Science 2013 (CS2013), began. Considerable work on the new volume has already been completed and a first draft of the CS2013 report (known as the Strawman report) will be complete by the beginning of 2012. This panel seeks to update and engage the SIGCSE community in providing feedback on the Strawman report, which will be available shortly prior to the SIGCSE conference.

The ACM/IEEE-Computer Society CS2013 Computer Science Curricula task force is working to update the previous curricular guidelines published in 2008 and 2001. The CS2013 guidelines are scheduled to be published in the latter half of 2013. This special session is devoted to exploring the guidelines with an emphasis on migrating current curricula to curricula aligned with the new guidelines. A number of significant changes from the 2008 and 2001 guidelines have been made, including the addition of new knowledge areas (including Parallel and Distributed Computing and Security and Information Assurance) as well as the reorganization and refactoring of previous areas to create a Systems Fundamentals area and a Software Development Fundamentals area. These changes are intended to identify significant changes in the computing field over the past decade, look forward to future changes, provide greater flexibility in the design and implementation of Computer Science curricula, provide stronger guidance with respect to student outcomes, and provide diverse examples of fielded curricula.

Project retrospectives are an established "best practice" in software process improvement. As a tool for learning how to perform better as a development organization, retrospectives may provide an additional learning opportunity for students in software engineering project courses. This paper describes a project retrospective approach that has been adapted to the academic setting. Academic project retrospectives not only provide students with the opportunity to reflect on their project performance, it gives the instructor additional information on improving the delivery, management, and learning outcomes. Key elements and suggestions f or improvements of the retrospective are described.

Beginning over 40 years ago with the publication of Curriculum 68, the major professional societies in computing--ACM and IEEE-Computer Society--have sponsored various efforts to establish international curricular guidelines for undergraduate programs in computing. As the field has grown and diversified, so too have the recommendations for curricula. There are now guidelines for Computer Engineering, Information Systems, Information Technology, and Software Engineering in addition to Computer Science. These volumes are updated regularly with the aim of keeping computing curricula modern and relevant. In the Fall of 2010, work on the next volume in the series, Computer Science 2013 (CS2013), began. Considerable work on the new volume has already been completed and a first draft of the CS2013 report (known as the Strawman report) will be complete by the beginning of 2012. This panel seeks to update and engage the SIGCSE community in providing feedback on the Strawman report, which will be available shortly prior to the SIGCSE conference.

Following a roughly 10 year cycle, the Computing Curricula volumes have helped to set international curricular guidelines for undergraduate programs in computing. In the summer of 2010, planning for the next volume in the series, Computer Science 2013, began. This panel seeks to update and engage the SIGCSE community on the Computer Science 2013 effort. The development of curricular guidelines in Computer Science is particularly challenging given the rapid evolution and expansion of the field. Moreover, the growing diversity of topics in Computer Science and the integration of computing with other disciplines create additional challenges and opportunities in defining computing curricula. As a result, it is particularly important to engage the broader computer science education community in a dialog to better understand new opportunities, local needs, and novel successful models of computing curriculum. The last complete Computer Science curricular volume was released in 2001 [3] and followed by a review effort that concluded in 2008 [2]. While the review helped to update some of the knowledge units in the 2001 volume, it was not aimed at producing an entirely new curricular volume and deferred some of the more significant questions that arose at the time. The Computer Science 2013 effort seeks to provide a new volume reflecting the current state of the field and highlighting promising future directions through revisiting and redefining the knowledge units in CS, rethinking the essentials necessary for a CS curriculum, and identifying working exemplars of courses and curricula along these lines.

The Property Specification (Prospec) tool uses patterns and scopes defined by Dwyer et al., to generate formal specifications in Linear Temporal Logic (LTL) and other languages. The work presented in this paper provides improved LTL specifications for patterns and scopes over those originally provided by Prospec. This improvement comes in the efficiency of the LTL formulas as measured in terms of the number of states in the Büchi automaton generated for the formula. Minimizing the size of the Büchi automata for an LTL specification provides a significant improvement for model checking software systems using such tools as the highly acclaimed Spin model checker.

The Prospec software tool facilitates the construction of formal specifications in LTL by automating Dwyer’s Specification Pattern System as extended by Mondragon and Salamah. The LTL generation has been verified through the automated creation of a rigorous test set. Over 3 million test cases were generated and executed, providing extensive coverage of the system.

This chapter describes a two-semester software engineering course that is taught in a computer science program at the University of Texas at El Paso. The course is distinguished from other courses in that it is based on the Affinity Research Group (ARG) philosophy that focuses on the deliberate development of students’ team, professional and technical skills within a cooperative environment. To address the challenge of having to teach professional and team skills as well as software engineering principles, approaches, techniques, and tools in a capstone course, the authors have defined an approach that uses a continuum of instruction, practice, and application with constructive feedback loops. The authors hope that the readers will benefit from the description of the approach and how ARG components are incorporated into the course.

Design decisions and constraints of a software system can be specified precisely using a formal notation such as the Object Constraint Language (OCL). However, they are not executable, and assuring the conformance of an implementation to its design is hard. The inability of expressing design constraints in an implementation and checking them at runtime invites, among others, the problem of design drift and corrosion. We propose runtime checks as a solution to mitigate this problem. The key idea of our approach is to translate design constraints written in a formal notation such as OCL into aspects that, when applied to a particular implementation, check the constraints at run-time. Our approach enables runtime verification of design-implementation conformance and detects design corrosion. The approach is modular and plug-and-playable; the constraint checking logic is completely separated from the implementation modules which are oblivious of the former. We believe that a significant portion of constraints translation can be automated.

This paper presents a formal correctness proof for some properties of restricted finite directed acyclic graphs (DAGs). A restricted graph has a single root and arbitrary siblings. The siblings are assigned integers, string values, or restricted DAGs. Leafs must be assigned string values. The main property is the transitive closure . Our restricted graphs and the properties are formalized in ACL2, and an ACL2 book has been prepared for reuse.

NOTE: The first page of text has been automatically extracted and included below in lieu of an abstract Experiment to Evaluate Teaching Formal Specifications Using Model Checking Salamah Salamah Computer and Software Engineering Dept., Embry-Riddle Aeronautical University. Steve Roach, Veronica Medina, Omar Ochoa, and Ann Gates Computer Science Dept., University of Texas at El Paso. Abstract The difficulty of writing, reading, and understanding formal specifications remains one of the main obstacles in adopting formal verification techniques such as model checking, theorem and runtime verification. In order to train a future workforce that can develop and test high-assurance systems, it is essential to introduce undergraduate students in computer science and software en- gineering to the concepts in formal methods. This paper presents an experiment that we used to validate the effectiveness of a new approach that can be used in an undergraduate course to teach formal approaches and languages. The paper presents study that was conducted at two institutions to compare the new approach with the traditional one in teaching formal specifications. The new approach uses a model checker and a specification tool to teach Linear Temporal Logic (LTL), a specification language that is widely used in a variety of verification tools. 1 Introduction In software engineering, formal techniques such as software runtime monitoring [5], and model checking [3, 8] require formal specifications that are based on mathematics. Formally specifying the behavior of a software system, however, is a difficult task because it requires mathematical sophis- tication to accurately specify, read, and understand properties written in a formal language. Natural language descriptions of software requirements are inherently ambiguous and often incomplete. Deriving a formal specification from a requirement written in natural-language of concurrent or sequential behavior is made more difficult because of the variety of aspects that must be considered when specifying software behavior. As such, a major impediment to the use of formal approaches in software development remains the difficulty associated with the development of correct formal specifications (i.e, ones that match the specifier’s original intent) [6, 7]. Currently, there exists multiple formal specification languages that can be used in a variety of verification techniques and tools. Linear Temporal Logic (LTL) [11], Computational Tree Logic (CTL) [10], and Meta Event Definition Language (MEDL) [9] are some of these languages. The aforementioned languages can be used in a variety of verification techniques and tools. For exam- ple, the model checkers SPIN [8] and NuSMV [2] use LTL to specify properties of software and hardware systems. On the other hand, the SMV [3] model checker verifies system behaviors against formal properties in in CTL. MEDL is used by JavaMac in runtime monitoring of java programs [9]. Many undergraduate curricula do not include the topic of formal methods. Certainly, a high level of mathematical sophistication is required for writing, reading, and understanding formal specifi- 1