Vendor Training for SELA Component
This presentation covers updates, guidance, and rules for the Special Education Language Acquisition (SELA) program. It includes information on submission updates, data element updates, code table revisions, and new business rules for the 2023-2024 school year. Also highlighted are key reminders for reporting student data accurately.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
From Program Verification to Program Synthesis Saurabh Srivastava * Sumit Gulwani Jeffrey S. Foster * * University of Maryland, College Park Microsoft Research, Redmond
Program Synthesis Goal: Automatically generate program Important benefits of program synthesis Reduced programmer burden Potential to generate novel algorithms Objective: Automatic program synthesis, given Pre/post condition (functional specification) Some hints about the form of the program scaffold Ideally: program is automatically proved correct Synthesized programs can be complicated
Proof-theoretic synthesis Our approach: Synthesize program and proof simultaneously Benefits: View synthesis as generalized verification Reuse existing verification tools and technology Tool synthesizes: linear arithmetic programs, sorting, dynamic programming programs
Discrete Line Drawing Input (X,Y) 0<Y X (12,7) (10,6) (11,6) (8,5) (9,5) (6,4) (7,4) Output values (5,3) |y-(Y/X)x| 1/2 (3,2) (4,2) (0,0) Using only linear operations: Bresenham s line drawing algorithm (0,0) (2,1) (1,1)
Synthesis Scaffold and Task The synthesis problem is described using a scaffold of the form <F,D,R> F: Functional Specification D: Domain Constraints R: Resource Constrains
Scaffold(1): Functional Specification Fuctional specification: (Fpre, Fpost) Precondition Fpre Formal specification of possible valid inputs E.g., 0<Y X Output Postcondition Fpost Formal specification that outputs need to meet E.g., |y-(Y/X)x| 1/2
Scaffold(2): Domain Constraints The domain specification: (Dexp, Dgrd,Dprf) Domains for program elements Expressions Dexp Guards Dgrd E.g. linear or quadratic expression over program variables predicates with array lookups Domain for invariants Dprf Choice of solver E.g., linear arithmetic Invariant form: iaix+biy+ci 0 Linear arithmetic fixed-point computation tool, i.e., verifier
Scaffold(3): Resource Constraints Hints about the form of the desired program (R loop, R stack, R comp) Looping structure R loop Acyclic fragments (*), loops ( ), sequencing (;) Grammar: L ::= | *(L) | L;L E.g., Acyclic fragment followed by a loop with an acyclic fragment inside * Stack R stack Maximum number of local variables permitted E.g., R stack =int, 1 Only one extra local variable is available
Synthesis Task Given a scaffold, the executable program valid if it meet the following conditions: input terminates: the program with invariants and ranking functions providing the proof Program loop corresponds to loop annotation in flowgraph template Program contains statements: S :: = skip | S;S | x := e | if g then S else S Element operation as many as Rcomp Program uses many local variable Rstack
Example: Integral Square root A scaffold with F = (? 1, ? 12 ? < ?2) computes the integral square root of the input ????,????be limited to linear arithmetic ?????,??????,????? be o;*(o);o, {(int, 1)}, E.g., IntSqrt(int x) { Invariant ?: v :=1; i:=1; ? = ?2 ? ? 12 ? 1 while?,? ? ? | v:= v+2i+1; i++; Ranking function: return i-1; } Where v, i are additional stack variable and iteration and counter ? ? 12
Outline Input: Scaffold Approach: Synthesis conditions Experiments
Modeling Basic Blocks as Transitions Task: Model statements in a manner that a solver can reason about State update and ordering problematic Basic Block as input->output transition inputs: v,x,Y outputs: v ,x v := v + 2Y; x++; transition : i(output vari = fn(input vars)) v = v + 2Y x = x + 1; Sbody : Example: {????} ? ??;? ??{?????} {????} <x ,y >=<??,??> {? ????} Verification condition: ???? ? = ?? ? = ?? ? ????
Synthesis Task p ::= choose {[]?? ??} | ? ??? , (g) do {p} | p;p Transition System Language: Example: (Integral square root computation) ; *( ); expand choose {[]g1 s1} ; ? ????|? while , (g0) { g1 , g2, g3 ????|? choose {[]g2 s2} ; s1 , s2, s3 ? ??= ?? }; ?? ?,?? ????|? choose {[]g3 s3}
VC - Safety Constraints Verification condition (VC) 0<Y X Sinit I I Gloop |y-(Y/X)x| 1/2 I Gcond1 Sbody1 I I Gcond2 Sbody2 I entry: output: 0<Y X Sinit while ( Gloop ) { |y-(Y/X)x| 1/2 []Gcond1 Sbody1 []Gcond2 Sbody2 } induct: output I entry induct
Fixed point solutions, i.e., invariants Verification condition (VC) 0<Y X Sinit I I Gloop |y-(Y/X)x| 1/2 I Gcond1 Sbody1 I I Gcond2 Sbody2 I entry: output: verifier induct: Domain specific reducer SAT solver ik, i.e., invariant I Assume a form for I,e.g., i1x+i2y+i3 0 for I (given the domains) Gcond2 boolean clauses linear arithmetic i1x+i2y+i3 0 Sbody2 i1x +i2y +i3 0 Linear arithmetic tricks integer SAT instance ik: linear arithmetic [PLDI 08] predicate abstraction [PLDI 09]
Fixed point solutions, i.e., invariants Verification condition (VC) 0<Y X Sinit I I Gloop |y-(Y/X)x| 1/2 I Gcond1 Sbody1 I I Gcond2 Sbody2 I entry: output: verifier induct: Domain specific reducer SAT solver ik, i.e., invariant I Assume a form for I,e.g., i1x+i2y+i3 0 for I (given the domains) Gcond2 boolean clauses linear arithmetic i1x+i2y+i3 0 Sbody2 i1x +i2y +i3 0 Linear arithmetic tricks integer SAT instance ik: linear arithmetic [PLDI 08] predicate abstraction [PLDI 09]
Unknown statements and guards Synthesize statements and guards! Verification condition (VC) 0<Y X Sinit I I Gloop |y-(Y/X)x| 1/2 I Gcond1 Sbody1 I I Gcond2 Sbody2 I entry: output: verifier induct: Domain specific reducer SAT solver ik, i.e., invariant I Assume a form for I, Gcond2,Sbody2,e.g., i1x+i2y+i3 0 for I (given the domains) boolean clauses linear arithmetic i1x+i2y+i3 0 g1x+g2y+g3 0 x =s1x+s2y+s3 y = i1x +i2y +i3 0 gk and sk guards/ statements Linear arithmetic tricks integer SAT instance ik,gk,sk: linear arithmetic [PLDI 08] predicate abstraction [PLDI 09]
Additional Constraints 0<Y X Sinit I I Gloop |y-(Y/X)x| 1/2 I Gcond1 Sbody1 I I Gcond2 Sbody2 I Termination Issue: Termination constraints Outputs reachable/termination constraints: Exists ranking function r r bounded from below r decreases in each iteration Safety Issue: Well-formedness not ensured Statements Well-formedness Conditional Guards Well-formedness constraints Conditional guards form tautologies Infer I and Sinit,Sbody1,Sbody2,Gloop,Gcond
Additional Constraints Synthesis Conditions User input: Scaffold User input: Program 0<Y X Sinit I I Gloop |y-(Y/X)x| 1/2 I Gcond1 Sbody1 I I Gcond2 Sbody2 I Termination VCGen SCGen Safety Verification Conditions Synthesis Conditions Fixed-pt Solver Fixed-pt Solver Well-formedness Synthesized Program+ Proof Verified Program + Proof Synthesis Verification (Invariant inference) Infer I and (Invariant + Program inference) Sinit,Sbody1,Sbody2,Gloop,Gcond Solving synthesis conditions does yield valid programs
Outline Input: Scaffold Approach: Synthesis conditions Experiments
Experiments: Linear Arithmetic LIA verifier from previous work [PLDI 08] Benchmarks Strassen s 2x2 matrix multiplication R loop = * and R stack = 7 --- for holding the seven intermediate results Swapping two integers without a temporary R loop = * and R stack = 0 Computing the integral square root Linear search R loop = *; (*) and R stack = 1 Binary search R loop = *; (*) and R stack = 2 Discrete line drawing R loop = *; (*) and R stack = 1
Experiments: Predicate Abstraction Predicate abstraction verifier from previous work [PLDI 09] Benchmarks: Sorting Requires quantified specification and invariants E.g., All major sorting programs Specification: sortedness Vary resource constraints Nested loop, 0 extra variables: bubble sort, insertion sort Nested loop, 1 extra variable: selection sort Recursive, 0 extra variables: merge sort Recursive, 1 extra variable: quick sort Benchmarks: Dynamic Programming Iterative program from its recursive specification E.g., Fibonacci Specification f(0)=1, f(1)=1, k>2: f(k)=f(k-1)+f(k-2) R loop = *; (*) and R stack = 2 Generated program maintains sliding window (of size 2) and computes f(n)
Experiments: Synthesis times 10,000,000 1 around 10,000 seconds 1,000,000 8 under 1000 seconds 100,000 seconds (log scale) 10,000 8 under 10 seconds 1,000 0.1 100 Verification Synthesis 0.01 10 0.001 1 LIA verifier Predicate abstraction verifier
Summary: Proof-theoretic synthesis Proof-theoretic synthesis Synthesize programs and proof simultaneously Treat synthesis as generalized verification Principled approach to solving for programs using verification User input: scaffold Functional specification Space of desired program Domains of guards and statements Resource constraints Approach: One-shot synthesis, i.e., no iteration Constraints, synthesis conditions, encode the desired program Safety, termination, and well-formedness Solve using existing constraint-based verifiers Possible to synthesize wide variety of programs
