We present verification of a bare-metal server built using diverse implementation techniques and languages against a whole-system input-output specification in terms of machine code, network packets, and mathematical ...
详细信息
We present verification of a bare-metal server built using diverse implementation techniques and languages against a whole-system input-output specification in terms of machine code, network packets, and mathematical specifications of elliptic-curve cryptography. We used very different formal-reasoning techniques throughout the stack, ranging from computer algebra, symbolic execution, and verification-condition generation to interactive verification of functional programs including compilers for C-like and functional languages. All these component specifications and domain-specific reasoning techniques are defined and justified against common foundations in the Coq proof assistant. Connecting these components is a minimalistic specification style based on functional programs and assertions over simple objects, omnisemantics for program execution, and basic separation logic for memory layout. This design enables us to bring the components together in a top-level correctness theorem that can be audited without understanding or trusting the internal interfaces and tools. Our case study is a simple cryptographic server for flipping of a bit of state through public-key authenticated network messages, and its proof shows total functional correctness including static bounds on memory usage. This paper also describes our experiences with the specific verification tools we build upon, along with detailed analysis of reasons behind the widely varying levels of productivity we experienced between combinations of tools and tasks.
Generating meaningful assert statements is one of the key challenges in automated test case generation,which requires understanding the intended functionality of the tested ***,deep learning based models have shown pr...
详细信息
Generating meaningful assert statements is one of the key challenges in automated test case generation,which requires understanding the intended functionality of the tested ***,deep learning based models have shown promise in improving the performance of assert statement ***,the existing models only rely on the test prefixes along with their corresponding focal methods,yet ignore the developer-written *** on our observations,the summarization contents usually express the intended program behavior or contain parameters that will appear directly in the assert *** information will help existing models address their current inability to accu-rately predict assert *** paper presents a summarization-guided approach for automatically generating as-sert *** derive generic representations for natural language(i.e.,summarization)and programming language(i.e.,test prefixes and focal methods),we leverage a pre-trained language model as the reference architecture and fine-tune it on the task of assert statement *** the best of our knowledge,the proposed approach makes the first at-tempt to leverage the summarization of focal methods as the guidance for making the generated assert statements more *** demonstrate the effectiveness of our approach on two real-world datasets compared with state-of-the-art mod-els.
We developed an information system using an object-oriented programming language and a distributed database (DDB) consisting of multiple interconnected databases across a computer network, managed by a distributed dat...
详细信息
As English becomes the mainstream language in communication and education worldwide, more and more Chinese universities emphasize the importance of adding English content to the higher education curriculum. This paper...
详细信息
Topological optimization plays a guiding role in the conceptual design *** paper conducts research on structural topology optimization algorithm within the framework of isogeometric *** multi-component structures,the ...
详细信息
Topological optimization plays a guiding role in the conceptual design *** paper conducts research on structural topology optimization algorithm within the framework of isogeometric *** multi-component structures,the Nitsche’smethod is used to glue differentmeshes to performisogeometricmulti-patch *** discrete variable topology optimization algorithm based on integer programming is adopted in order to obtain clear boundaries for topology *** sensitivity filtering method based on the Helmholtz equation is employed for averaging of curved elements’*** addition,a simple averaging method along coupling interfaces is proposed in order to ensure the material distribution across coupling areas is reasonably ***,the performance of the algorithm is demonstrated by numerical examples,and the effectiveness of the algorithm is verified by comparing it with the results obtained by single-patch and ABAQUS cases.
作者：
Hicks, AlexShi, YangLekshmi-Narayanan, Arun-BalajieeYan, WeiMarwan, SamihaDept of Computer Science
Virginia Tech Blacksburg VA Dept of Computer Science Utah State University Logan UT Intelligent Systems Program University of Pittsburgh Pittsburgh PA School of Informatics Computing and Cyber Systems North Arizona University Flagstaff AZ Dept. of Computer Science University of Virginia wCharlottesville VA
Students’ interactions while solving problems in learning environments (i.e. log data) are often used to support students’ learning. For example, researchers use log data to develop systems that can provide students...
详细信息
Rigorous, mathematical reasoning, i.e., proof, is the foundation of any undergraduate computerscience education. However, students find mathematical proof exceedingly challenging, but also at the same time do not see...
详细信息
ISBN:
(纸本)9781450394338
Rigorous, mathematical reasoning, i.e., proof, is the foundation of any undergraduate computerscience education. However, students find mathematical proof exceedingly challenging, but also at the same time do not see its relevance to programming. We address these concerns with SNOWFLAKE, an educational proof assistant designed to help undergraduates overcome these difficulties when authoring mathematical proof. SNOWFLAKE does this by operating in a context where mathematical proof is introduced alongside programming in either a CS1 or CS2 context. The lens that we use to unite the two concepts is program correctness, a topic that immediately makes relevant the concept of formal reasoning as students are perpetually faced with the issue of whether their code is correct. SNOWFLAKE is a proof assistant designed for the needs of undergraduates in courses that closely time programming and proof. It is a web-based application that helps students author proofs not only in the context of program correctness in-the-small, but also other topics found in discrete mathematics courses. We report on the design of SNOWFLAKE, the kinds of reasoning it enables, and our plans to deploy SNOWFLAKE in the classroom.
With the development of computerscience and artificial intelligence technology, automatic scoring algorithms have become a highly concerned research field in the education industry. Especially in computerprogramming...
详细信息
Productive Failure (PF) is a learning approach where students initially tackle novel problems targeting concepts they have not yet learned, followed by a consolidation phase where these concepts are taught. Recent app...
详细信息
ISBN:
(纸本)9798400705311
Productive Failure (PF) is a learning approach where students initially tackle novel problems targeting concepts they have not yet learned, followed by a consolidation phase where these concepts are taught. Recent application in STEM disciplines suggests that PF can help learners develop more robust conceptual knowledge. However, empirical validation of PF for programming education remains under-explored. In this paper, we investigate the use of PF to teach Python lists to undergraduate students with limited prior programming experience. We designed a novel PF-based learning activity that incorporated the unobtrusive collection of real-time heart-rate data from consumer-grade wearable sensors. This sensor data was used both to make the learning activity engaging and to infer cognitive load. We evaluated our approach with 20 participants, half of whom were taught Python concepts using Direct Instruction (DI), and the other half with PF. We found that although there was no difference in initial learning outcomes between the groups, students who followed the PF approach showed better knowledge retention and performance on delayed but similar tasks. In addition, physiological measurements indicated that these students also exhibited a larger decrease in cognitive load during their tasks after instruction. Our findings suggest that PF-based approaches may lead to more robust learning, and that future work should investigate similar activities at scale across a range of concepts.
In a typical introductory programming course, grading student-submitted programs involves an autograder which compiles and runs the programs and tests their functionality with predefined test cases, with no attention ...
详细信息
ISBN:
(纸本)9798400705328
In a typical introductory programming course, grading student-submitted programs involves an autograder which compiles and runs the programs and tests their functionality with predefined test cases, with no attention to the source code. However, in an educational setting, grading based on inspection of the source code is required for two main reasons (1) awarding partial marks to 'partially correct' code that may be failing the testcase check (2) awarding marks (or penalties) based on source code quality or specific criteria that the instructor may have laid out in the problem statement (e.g. 'implement sorting using bubble-sort'). However, grading based on studying the source code can be highly time consuming when the course has a large enrollment. In this paper we present the design and evaluation of an AI Assistant for source code grading, which we have named TA Buddy. TA Buddy is powered by Code Llama, a large language model especially trained for code related tasks, which we fine-tuned using a graded programs dataset. Given a problem statement, student code submissions and a grading rubric, TA Buddy can be asked to generate suggested grades, i.e. ratings for the various rubric criteria, for each submission. The human teaching assistant (TA) can then accept or overrule these grades. We evaluated the TA Buddy-assisted manual grading against 'pure' manual grading and found that the time taken to grade reduced by 24% while maintaining grade agreement in the two cases at 90%.
暂无评论